Groupoids internal to assemblies on a partial combinatory algebra form a pi-tribe, hence a model of dependent type theory, with a model structure, W-types, a univalent impredicative universe, and 0-type homotopy category RT[A].
The algebraic internal groupoid model of Martin-L\"{o}f type theory
1 Pith paper cite this work. Polarity classification is still indexing.
abstract
We extend the model structure on the category $\mathbf{Cat}(\mathcal{E})$ of internal categories studied by Everaert, Kieboom and Van der Linden to an algebraic model structure. Moreover, we show that it restricts to the category of internal groupoids. We show that in this case, the algebraic weak factorisation system that consists of the algebraic trivial cofibrations and algebraic fibrations forms a model of Martin-L\"{o}f type theory. Taking $\mathcal{E} = \mathbf{Set}$ and forgetting the algebraic structure, this recovers Hofmann and Streicher's groupoid model of Martin-L\"{o}f type theory. Finally, we are able to provide axioms on a $(2,1)$-category which ensure that it gives an algebraic model of Martin-L\"{o}f type theory. To do this, we give necessary and sufficient axioms on a $2$-category $\mathcal{K}$ such that $\mathcal{K} \simeq \mathbf{Cat}(\mathcal{E})$ in which $\mathcal{E}$ is a locally cartesian closed locos with coequalisers, a result which we believe is of independent interest.
fields
math.CT 1years
2025 1verdicts
CONDITIONAL 1representative citing papers
citing papers explorer
-
A Model of Type Theory in Groupoid Assemblies
Groupoids internal to assemblies on a partial combinatory algebra form a pi-tribe, hence a model of dependent type theory, with a model structure, W-types, a univalent impredicative universe, and 0-type homotopy category RT[A].