We develop realizability models of intensional type theory, based on groupoids, wherein realizers themselves carry non-trivial (non-discrete) homotopical structure. In the spirit of realizability, this is intended to formalize a homotopical BHK interpretation, whereby evidence for an identification is a path. Specifically, we study partitioned groupoidal assemblies. Categories of such are parameterised by "realizer categories" (instead of the usual partial combinatory algebras) that come equipped with an interval qua internal cogroupoid. The interval furnishes a notion of homotopy as well as a fundamental groupoid construction. Objects in a base groupoid are realized by points in the fundamental groupoid of some object from the realizer category; isomorphisms in the base groupoid are realized by paths in said fundamental groupoid. The main result is that, under mild conditions on the realizer category, the ensuing category of partitioned groupoidal assemblies models intensional (1-truncated) type theory without function extensionality. Moreover, when the underlying realizer category is "untyped", there exists an impredicative universe of 1-types (the modest fibrations). This is a groupoidal analogue of the traditional situation.

翻译：我们基于群胚发展了内涵类型论的实现性模型，其中实现子自身携带非平凡（非离散）的同伦结构。秉承实现性思想，这旨在形式化同伦BHK解释，即等同性的证据是一条路径。具体而言，我们研究分划群胚装配。此类范畴由"实现子范畴"（取代通常的部分组合代数）参数化，这些范畴配备有一个作为内部余群胚的区间对象。该区间提供了同伦概念以及基本群胚构造。基础群胚中的对象由实现子范畴中某对象的基本群胚中的点实现；基础群胚中的同构由所述基本群胚中的路径实现。主要结果表明，在对实现子范畴的温和条件下，由此产生的分划群胚装配范畴能够建模不含函数外延性的内涵（1-截断）类型论。此外，当底层实现子范畴为"无类型"时，存在一个1-类型（适度纤维化）的直谓宇宙。这是传统情况的群胚类比。