Pith. sign in

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

arxiv 2503.17319 v2 pith:5POVKWS7 submitted 2025-03-21 math.CT math.LO

classification math.CTmath.LO
keywords algebraicmathcalmodelcategorymartin-ltheorytypeinternal
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. A Model of Type Theory in Groupoid Assemblies

    math.CT 2025-07 conditional novelty 7.0 of 10

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

Pith tools