Pith. sign in

The algebraic internal groupoid model of Martin-L\"{o}f type theory

1 Pith paper cite this work. Polarity classification is still indexing.

1 Pith paper citing it
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 1

years

2025 1

verdicts

CONDITIONAL 1

representative citing papers

A Model of Type Theory in Groupoid Assemblies

math.CT · 2025-07-21 · conditional · novelty 7.0

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].

citing papers explorer

Showing 1 of 1 citing paper.

  • A Model of Type Theory in Groupoid Assemblies math.CT · 2025-07-21 · conditional · none · ref 14 · internal anchor

    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].