REVIEW 1 cited by
The algebraic internal groupoid model of Martin-L\"{o}f type theory
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
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.
Forward citations
Cited by 1 Pith paper
-
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 categ...
Discussion (0). Continue with ORCID to comment.