Pith. sign in

REVIEW 3 major objections 5 minor 47 references

A 2-categorical approach to the semantics of dependent type theory with computation axioms

T0 review · 3 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Display map 2-categories give a sound semantics for axiomatic type theory, and a weakened groupoid model shows the identity-type computation rule is not admissible.

desk verdict Genuinely new 2-categorical semantics for axiomatic type theory with a plausible independence result, but Section 5 needs a real proof of the compatibility claims before Theorem 5.1 should be trusted. read the letter →

arxiv 2507.07208 v1 pith:VFLKSUOY submitted 2025-07-09 math.LO cs.LOmath.CT

Matteo Spadetto This is my paper · ORCID
classification math.LOcs.LOmath.CT MSC 03B1503G3018N10
keywords axiomatictypetheorycomputationaxiomsdependentdisplaymap2-categoriescategoricalsemanticsgroupoidmodelidentitytypesfunctionextensionality
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Axiomatic type theory (ATT) is the variant of dependent type theory in which each type former's computation rule is downgraded from a judgemental equality, like $t \equiv t'$, to a propositional equality, like $p : t = t'$, called a computation axiom. This paper proves that such theories have a uniform 2-categorical semantics: every display map 2-category equipped with axiomatic identity, $\Sigma$-, $\Pi$-, function extensionality, and 0-, 1-, 2-, $N$-types induces an ordinary display map category that models ATT, and that interpretation is sound. The proof works by encoding each axiomatic type former as a 2-dimensional universal property, so that the 1-dimensional choice functions needed for a syntactic model arise automatically. As an application, a weakened groupoid model in which types are pseudofunctors into the category of groupoids models axiomatic identity types without validating their judgemental computation rule, establishing that the computation rule of identity types is not admissible in ATT. If the paper is right, checking a handful of 2-categorical properties is enough to build models of very intensional dependent type theories, and a specific meta-theoretic independence question is settled.

What carries the argument

The load-bearing object is the display map 2-category: a $(2,1)$-category whose chosen display maps are cloven isofibrations, with a split re-indexing structure and, for identity types, an arrow object $\alpha_A$ for each display map $P_A$ that represents 2-cells between sections of $P_A$ as sections of the identity-type display map. The arrow object is what turns the syntax of axiomatic identity types into data: elimination terms are first built as 'pseudo-terms' whose codomain is a display map only up to a 2-cell, and the cloven isofibration structure strictifies them into genuine sections while producing exactly the 2-cells that are then read as computation axioms. Relaxing normal isofibrations to merely cloven ones is what keeps the computation axioms from collapsing into the judgemental computation rules. The same machinery, with homotopy equivalences, biadjoints, and bireflections in place of their retract versions, encodes the remaining axiomatic type formers.

What would settle it

Take a non-strict pseudofunctor in the weakened groupoid model and compute the re-indexing pastings and isofibration transport required by Definitions 4.1 and 4.2; if any required equality fails, the model is not a display map 2-category and Theorem 5.1 collapses. Separately, any derivation in ATT of the judgemental equality $J(c,x,x,r(x)) \equiv c(x)$ would directly refute the paper's main non-admissibility claim.

Watch

Extended reading notes

Core claim

The central claim is that the intensional type formers of axiomatic type theory admit a 2-categorical description, and that this description is strong enough to carry the semantics. Concretely, axiomatic identity types are encoded by arrow objects for display maps, axiomatic $\Sigma$-types by closure of display maps under composition up to homotopy equivalence, axiomatic $\Pi$-types and function extensionality by a right biadjoint, and axiomatic 0-, 1-, 2-, $N$-types by bireflections. Any display map 2-category carrying these structures induces a split display map category with all the choice functions of Definitions 3.1--3.5, so by the standard soundness argument the interpretation of ATT is well defined and sound (Theorems 3.6 and 4.11). The decisive application is a display map 2-category based on the groupoid model in which display maps are cloven, but not necessarily normal, isofibrations: it validates axiomatic identity types and their computation axiom, yet fails the judgemental computation rule $J(c,x,x,r(x)) \equiv c(x)$, proving that rule is not admissible in ATT (Theorem 5.1).

Load-bearing premise

The load-bearing premise is that the weakened groupoid model of Section 5 really is a display map 2-category: the paper asserts, without proving, that its re-indexing, cloven isofibration, and arrow-object structures satisfy all the compatibility laws of Definitions 4.1 and 4.2, and the independence result rests on that.

Editorial extensions

If this is right

  • Any display map 2-category endowed with the listed axiomatic type-former data is automatically a model of ATT, so model construction reduces to checking 2-dimensional universal properties rather than choosing interpretation functions rule by rule.
  • The interpretation is sound: in any such structure every derivable judgement of ATT receives a well-defined denotation, and judgemental equalities are respected.
  • The weakened groupoid model $(\mathrm{Grpd}, D)$ is a model of axiomatic identity types that does not validate the computation rule for identity types; hence that rule is not admissible in ATT.
  • Every display map 2-category validates the discreteness rule, so the semantics is sound for ATT plus discreteness; because that rule is not derivable in ATT, this class of models cannot be complete for ATT alone.
  • If, in the same data, all the equivalence 2-cells are identities and the display maps are normal isofibrations, the induced model validates the full intensional computation rules and is a model of ITT.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper leaves implicit that the discreteness obstruction is a feature of any 2-categorical display-map semantics: the arrow object forces a type to behave like a 1-type, so a complete semantics for ATT without discreteness will have to go one dimension higher, as the paper's own closing discussion suggests.
  • One testable extension is to apply the same encoding to directed identity types: replacing arrow objects by directed hom-objects in a display map 2-category should produce a model of directed versions of ATT, paralleling existing categorical models of directed type theory.
  • Because the weakened groupoid model separates the computation axiom from the computation rule by the strictness of the pseudofunctor, one can vary the pseudofunctor to generate further independence results, including analogous $\Sigma$ or $\Pi$ computation rules, although the paper only carries out the identity-type case.
  • Since type checking in ATT is already known to be decidable in quadratic time, a practical consequence is that 2-categorical models could serve as the underlying denotational description for implementations of objective type theory; this is an inference, not a claim of the paper.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper develops a 2-categorical semantics for axiomatic type theory (ATT), a dependent type theory in which computation rules are replaced by propositional computation axioms. It introduces display map 2-categories, a 2-dimensional analogue of display map categories, and shows that a display map 2-category endowed with axiomatic identity, Σ, Π, 0, 1, 2, and N types and function extensionality induces an ordinary display map category that is a model of ATT (Theorem 4.11). The paper then proposes a weakened groupoid model, claims it is a display map 2-category with axiomatic identity types, and concludes that it fails the intensional computation rule for identity types, so that rule is not admissible in ATT (Theorem 5.1). Section 6 shows that every such model validates the discreteness rule and uses a syntactic display map 2-category, imported from the author's thesis, to state a completeness theorem for ATT plus discreteness.

Significance. The paper's conceptual contribution is attractive: encoding computation axioms as relaxed 2-categorical universal properties, rather than 1-categorical ones, yields a semantics that generalizes Garner's intensional models and distinguishes axiomatic from intensional type formers. The explicit stability conditions and the appendices show care in the syntactic-to-categorical passage. The weakened groupoid model, if fully verified, would provide a clean semantic proof that the intensional computation rule is not admissible in ATT. However, as it stands, the verification that the groupoid model is a display map 2-category is asserted rather than proved, and a number of stability proofs needed for Theorem 4.11 are deferred or only sketched. The central idea is sound and the missing material appears to be fillable, but the current manuscript is not yet self-contained at the load-bearing points.

major comments (3)
  1. [Section 5, 'Re-indexing structure and arrow object structure on display maps'; Appendix C] Theorem 5.1, the paper's headline independence result, depends on (Grpd, D) being a display map 2-category in the sense of Definition 4.1. The text says 'Without delving too deeply into the details, we state that...' and Appendix C only says that the cloven isofibration structure 'is compatible with this re-indexing choice in the sense of Definition 4.1' and that the arrow object 'can be verified to be compatible with the re-indexing choice in the sense of Definition 4.2.' No proof is given for the crucial fourth condition of Definition 4.1, namely the equalities t^p_g[f.A] = t^{p[f]}_{g'} and τ^p_g[f.A] = τ^{p[f]}_{g'} for the chosen cloven isofibration lifts. Since Theorem 5.1 relies on this structure to induce a model of axiomatic identity types, this is a load-bearing gap. Please supply the full verification, or a precise reference where it is carried out.
  2. [Appendix B; Propositions 4.5 and 4.10] Theorem 4.11 asserts that every display map 2-category with the axiomatic type-former data induces a display map category with the corresponding syntactic data, and the proof of that theorem rests on Propositions 4.3, 4.5, 4.8, and 4.10. Appendix B proves Proposition 4.3 and parts of Proposition 4.8, but Proposition 4.5 (for Σ-types) and Proposition 4.10 (for 0-, 1-, 2-, N-types) are only declared to be 'completely analogous' or 'analogous.' These stability conditions are exactly what makes the induced display map category split, so they are essential for Theorem 4.11. The paper should include complete proofs of these propositions, or at least a detailed treatment of the non-obvious cases such as Σ and N.
  3. [Appendix C, computation of Jc[rA]] The proof of Theorem 5.1 hinges on the claim that 'following the construction at paragraphs Elim Rule and Comp Axiom for =-types, one can reconstruct the choice functions r, φ, and J and observe that Jc acts on objects as...' This calculation is asserted rather than derived, even though it depends on the specific chosen arrow object and cloven isofibration structure on the weakened groupoid model. Because the inequality Jc[rA] ≠ c is the entire content of the non-admissibility claim, the calculation should be presented explicitly or accompanied by a complete proof.
minor comments (5)
  1. [Definition 3.5, 2-types] In the Comp Axiom clauses for 2-types, the display map for β^{2,⊤}_{c,d} is written as Γ.Id_{C[⊤]}[ind^2_{c,d}[⊤]; c], and the displayed arrow is written as ind^2_{c,d}[⊤]; c; the second occurrence of c should be d.
  2. [Definition 4.9, 2-types] In the bullet for axiomatic 2-types, the 2-functor U is written as (D/Γ.1)† → (C/Γ.1)2; the context should be Γ.2, not Γ.1.
  3. [Section 2.1 and Appendix A] Diagram (10) is referenced in Section 2.1 before it is introduced in Appendix A; please add a forward reference or introduce the diagram earlier.
  4. [Section 6] The completeness theorem 6.3 is obtained by importing the syntactic display map 2-category and its type-former structure from the author's thesis [38], with only a sentence saying that the remaining type formers can be handled analogously. Since this is a claimed theorem of the paper, please state explicitly which parts are new and which are cited, and consider expanding the proof if completeness is to be counted as a contribution.
  5. [Section 4.5] Theorem 4.12 is stated without a proof; the surrounding paragraphs give a helpful discussion but not a formal verification. Either provide a proof or label the statement as a remark.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the paper's central theorems are derived from explicitly stated 2-categorical structures rather than from their own conclusions, with the only notable caveat being an unproved coherence assertion in the groupoid model that is a correctness gap, not a circular reduction.

full rationale

I traced the claimed derivation chain. Theorem 3.6 is a standard induction over derivations using the choice functions of Definitions 3.1-3.5; its soundness does not presuppose any display map 2-category, and no fitted parameter is involved. The main construction, Theorem 4.11, takes the universal properties of Definitions 4.2, 4.4, 4.6 and 4.9 (arrow objects, homotopy equivalences, biadjoints and bireflections) and derives the syntactic choice functions (refl, J, H, split, sigma, abst, beta, etc.) from them; the derived data are not literally the postulated data, and the stability checks in Propositions 4.3, 4.5, 4.8 and 4.10 are proved in Appendix B from the assumed stability of the categorical data. This is a soundness construction, not an equation that reduces to its input. The independence result, Theorem 5.1, is a concrete model check in the groupoid model, with the non-coincidence Jc[rA] != c exhibited by an explicit object formula. The paper does contain a load-bearing unverified assertion: in Section 5 it says 'Without delving too deeply into the details, we state that the 1-cells of D can be endowed with a 1- and 2-dimensional re-indexing structure, as well as with a structure of arrow objects, such that the compatibilities outlined in the third and fourth points of Definition 4.1 are satisfied.' If those compatibilities fail, Theorem 5.1 collapses; but this is an omitted coherence proof, not a circular step, because the conclusion is not assumed by that assertion. Finally, Section 6's completeness theorem relies on the author's thesis [38] for the syntactic display map 2-category; this is a self-citation that is load-bearing for the ancillary completeness claim, but it is prior work with stated propositions, and neither the main soundness theorem nor the non-admissibility result reduces to it. I therefore find no step in which a prediction or first-principles result is equivalent by construction to its own input.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

The paper introduces no fitted parameters and no new postulated entities such as particles or forces. The central claim rests on the definitional framework of display map 2-categories and on standard 2-category theory. Several structural verifications, especially in the groupoid model, are asserted rather than fully proved, which is the main source of correctness risk.

assumptions (6)
  • domain assumption Definition 4.1: display map 2-category with cloven isofibrations and 2-pullbacks
    The central semantic structure is assumed to exist; Theorem 4.11 is relative to this definition.
  • domain assumption The standard syntax of ATT with computation axioms (Section 3, Figures 1-4)
    The theory being modeled is defined by these rules, including axiomatic Id, Sigma, Pi, function extensionality, 0, 1, 2, and N types.
  • domain assumption Existence of arrow objects (Definition 4.2) and right biadjoints (Definition 4.6) stable under re-indexing
    These universal properties are the categorical encodings of the type formers; they are required to hold and to be stable under substitution.
  • standard math Standard 2-category theory, including adjoint equivalences and pseudofunctor coherence (Bénabou, Lack, Gray)
    Used to assume adjoint equivalences for Sigma and for pseudo-inverses in the 0-, 1-, 2-, N-type bireflections.
  • domain assumption In the groupoid model, types are pseudofunctors into Grpd and the Grothendieck construction yields display maps
    This is the model construction; it relies on coherence laws of pseudofunctors and on the claim that the resulting structures satisfy Definition 4.1.
  • domain assumption The syntactic 2-category CATT+Disc from [38] is a display map 2-category
    Completeness (Theorem 6.3) relies on results from the author's thesis; these are cited but not reproven in this paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A 2-categorical approach to the semantics of dependent type theory with computation axioms." pith.science (2026). https://pith.science/paper/VFLKSUOY

@misc{pith2026250707208,
  author       = {Pith},
  title        = {Pith review of: A 2-categorical approach to the semantics of dependent type theory with computation axioms},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VFLKSUOY}},
  note         = {Machine review of arXiv:2507.07208}
}
read the original abstract

Axiomatic type theory is a dependent type theory without computation rules. The term equality judgements that usually characterise these rules are replaced by computation axioms, i.e., additional term judgements that are typed by identity types. This paper is devoted to providing an effective description of its semantics, from a higher categorical perspective: given the challenge of encoding intensional type formers into 1-dimensional categorical terms and properties, a challenge that persists even for axiomatic type formers, we adopt Richard Garner's approach in the 2-dimensional study of dependent types. We prove that the type formers of axiomatic theories can be encoded into natural 2-dimensional category theoretic data, obtaining a presentation of the semantics of axiomatic type theory via 2-categorical models called display map 2-categories. In the axiomatic case, the 2-categorical requirements identified by Garner for interpreting intensional type formers are relaxed. Therefore, we obtain a presentation of the semantics of the axiomatic theory that generalises Garner's one for the intensional case. Our main result states that the interpretation of axiomatic theories within display map 2-categories is well-defined and enjoys the soundness property. We use this fact to provide a semantic proof that the computation rule of intensional identity types is not admissible in axiomatic type theory. This is achieved via a revisitation of Hofmann and Streicher's groupoid model that believes axiomatic identity types but does not believe intensional ones.

Figures

Figures reproduced from arXiv: 2507.07208 by the authors.

Figure 1
Figure 1. Axiomatic =-types axioms. We will be focusing on the following type formers: =-types, Σ-types, Π-types, function extensionality, 0-types, 1-types, 2-types, and N-types. There are several motivations and advantages to work on ATT: ≻ Axiomatic type theory is objective [35, 44] in the way operations, such as the sum of natural numbers or the composition of identity proofs, can be defined. In ITT, depending on how the e… view at source ↗
Figure 2
Figure 2. Axiomatic Σ-types Definition 3.2 (Semantics of axiomatic Σ-types—syntactic formulation). Let (C, D) be a display map category endowed with axiomatic =-types. Let us assume that, for every object Γ, every display map PA of codomain Γ, and every display map PB of codomain Γ.A, there is a choice of: ≻ (Form Rule) a display map Γ.Σ B A → Γ; ≻ (Intro Rule) a section: pairB A : Γ.A.B → Γ.A.B.Σ B A[PAPB] of the display map… view at source ↗
Figure 3
Figure 3. Axiomatic Π-types & axiomatic function extensionality Moreover, let us assume that the following stability conditions: Σ B A[f] = Σ B[f • ] A[f] splitc [f • ] = splitc[f••] pairB A[f •• ] = pairB[f • ] A[f] σc[f •• ] = σc[f••] hold1 for every arrow f : ∆ → Γ. Then we say that (C, D) is endowed with axiomatic Σ-types. Now, referring to the rules of [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Axiomatic 0-, 1-, 2-, and N-types 14 [PITH_FULL_IMAGE:figures/full_fig_p014_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

47 extracted references · 46 canonical work pages

  1. [1]

    Ahrens, P

    B. Ahrens, P. R. North, and N. van der Weide. Semantics for two-dimensional type theory. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, pages [Article 12], 14. ACM, New York, [2022]©2022

    work page 2022

  2. [2]

    Ahrens, P

    B. Ahrens, P. R. North, and N. van der Weide. Bicategorical type theory: semantics and syntax. Math. Structures Comput. Sci., 33(10):868–912, 2023

    work page 2023

  3. [3]

    Altenkirch and J

    T. Altenkirch and J. Neumann. Synthetic 1-categories in directed type theory. arXiv:2410.19520, 2024

    arXiv 2024

  4. [4]

    S. Awodey. Natural models of homotopy type theory. Math. Structures Comput. Sci., 28(2):241–286, 2018

    work page 2018

  5. [5]

    Awodey, N

    S. Awodey, N. Gambino, and K. Sojakova. Inductive types in homotopy type theory. In Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 95–104. IEEE Computer Soc., Los Alamitos, CA, 2012

    work page 2012

  6. [6]

    Awodey, N

    S. Awodey, N. Gambino, and K. Sojakova. Homotopy-initial algebras in type theory.J. ACM, 63(6):Art. 51, 45, 2017

    work page 2017

  7. [7]

    J. Bénabou. Introduction to bicategories. In Reports of the Midwest Category Seminar, volume No. 47 ofLecture Notes in Math., pages 1–77. Springer, Berlin-New York, 1967

    work page 1967

  8. [8]

    Bezem, T

    M. Bezem, T. Coquand, and S. Huber. A model of type theory in cubical sets. In19th International Conference on Types for Proofs and Programs, volume 26 ofLIPIcs. Leibniz Int. Proc. Inform., pages 107–128. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2014

    work page 2014

Show all 47 references
  1. [9]

    R. Bocquet. Coherence of strict equalities in dependent type theories. arXiv:2010.14166, 2020

    2010 arXiv

  2. [10]

    Strictificationofweaklystabletype-theoreticstructuresusinggenericcontexts

    R.Bocquet. Strictificationofweaklystabletype-theoreticstructuresusinggenericcontexts. In 27th International Conference on Types for Proofs and Programs, volume 239 ofLIPIcs. Leibniz Int. Proc. Inform., pages Art. No. 3, 23. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2022

    2022

  3. [11]

    Boulier and T

    S. Boulier and T. Winterhalter. Weak type theory is rather strong.30th International Con- ference on Types for Proofs and Programs, 2019. https://www.ii.uib.no/~bezem/abstracts/ TYPES_2019_paper_18

    2019

  4. [12]

    Cartmell

    J. Cartmell. Generalised Algebraic Theories and Contextual Categories. PhD thesis, Uni- versity of Oxford, 1978

    1978

  5. [13]

    Clairambault and P

    P. Clairambault and P. Dybjer. The biequivalence of locally cartesian closed categories and Martin-Löf type theories. Mathematical Structures in Computer Science, 24(6):e240606, 2014

    2014

  6. [14]

    Cohen, T

    C. Cohen, T. Coquand, S. Huber, and A. Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom. In 21st International Conference on Types for Proofs and Programs, volume 69 ofLIPIcs. 2018

    2018

  7. [15]

    Coquand and N

    T. Coquand and N. A. Danielsson. Isomorphism is equality. Indag. Math. (N.S.), 24(4):1105–1120, 2013. 62

    2013

  8. [16]

    P. Dybjer. Internal type theory. InTypes for Proofs and Programs: International Work- shop, TYPES’95, Torino, Italy, June 5-8, 1995 Selected Papers, volume 1158, page 120. Springer Science & Business Media, 1996

    1995

  9. [17]

    R. Garner. Two-dimensional models of type theory. Math. Structures Comput. Sci., 19(4):687–736, 2009

    2009

  10. [18]

    J. W. Gray.Formal category theory: adjointness for2-categories, volume 391 ofLecture Notes in Mathematics. Springer-Verlag, Berlin-New York, 1974

    1974

  11. [19]

    N. Gurski. Coherence in three-dimensional category theory, volume 201 of Cambridge Tracts in Mathematics. Cambridge University Press, Cambridge, 2013

    2013

  12. [20]

    M. Hofmann. Extensional concepts in intensional type theory. PhD thesis, University of Edinburgh, 1995

    1995

  13. [21]

    M. Hofmann. On the interpretation of type theory in locally cartesian closed categories. In L. Pacholski and J. Tiuryn, editors,Computer Science Logic, pages 427–441, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg

    1995

  14. [22]

    M. Hofmann. Conservativity of equality reflection over intensional type theory. In S. Be- rardi and M. Coppo, editors,Types for Proofs and Programs, pages 153–164, Berlin, Hei- delberg, 1996. Springer Berlin Heidelberg

    1996

  15. [23]

    M. Hofmann. Syntax and semantics of dependent types, pages 13–54. Springer, London, 1997

    1997

  16. [24]

    Hofmann and T

    M. Hofmann and T. Streicher. The groupoid model refutes uniqueness of identity proofs. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994), pages 208–212. IEEE Computer Society Press, July 1994

    1994

  17. [25]

    Hofmann and T

    M. Hofmann and T. Streicher. The groupoid interpretation of type theory. InTwenty-five years of constructive type theory (Venice, 1995), volume 36 ofOxford Logic Guides, pages 83–111. Oxford Univ. Press, New York, 1998

    1995

  18. [26]

    B. Jacobs. Comprehension categories and the semantics of type dependency. Theoret. Comput. Sci., 107(2):169–207, 1993

    1993

  19. [27]

    B. Jacobs. Categorical logic and type theory, volume 141 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, 1999

    1999

  20. [28]

    Kapulkin and P

    K. Kapulkin and P. L. Lumsdaine. Homotopical inverse diagrams in categories with at- tributes. Journal of Pure and Applied Algebra, 225(4):106563, 2021

    2021

  21. [29]

    S. Lack. A 2-categories companion. In Towards Higher Categories, volume 152 ofIMA Vol. Math. Appl., pages 105–191. Springer, New York, 2010

    2010

  22. [30]

    P. L. Lumsdaine and M. A. Warren. The local universes model: an overlooked coherence construction for dependent type theories.ACM Trans. Comput. Log., 16(3):Art. 23, 31, 2015

    2015

  23. [31]

    E. Moggi. A category-theoretic account of program modules.Math. Structures Comput. Sci., 1(1):103–139, 1991. 63

    1991

  24. [32]

    Dialecticamodelsoftypetheory

    S.K.MossandT.vonGlehn. Dialecticamodelsoftypetheory. In 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, page 739–748, New York, NY, USA, 2018. Association for Computing Machinery

    2018

  25. [33]

    P. R. North. Towards a directed homotopy type theory. InProceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics, volume 347 of Electron. Notes Theor. Comput. Sci., pages 223–239. Elsevier Sci. B. V., Amsterdam, 2019

    2019

  26. [34]

    Otten and M

    D. Otten and M. Spadetto. Models for axiomatic type theory.Workshop on Homotopy Type Theory & Univalent Foundations, 2024. https://hott-uf.github.io/2024/abstracts/ HoTTUF_2024_paper_14.pdf

    2024

  27. [35]

    L. C. Paulson. Formalising mathematics in simple type theory. InReflections on the foun- dations of mathematics—univalent foundations, set theory and general thoughts, volume 407 ofSynth. Libr., pages 437–453. Springer, Cham, [2019]©2019

    2019

  28. [36]

    R. A. G. Seely. Locally Cartesian closed categories and type theory.Math. Proc. Cambridge Philos. Soc., 95(1):33–48, 1984

    1984

  29. [37]

    Spadetto

    M. Spadetto. Relating homotopy equivalences to conservativity in dependent type theories with propositional computation. arXiv:2303.05623, 2023

    2023

  30. [38]

    Spadetto

    M. Spadetto. On the syntax and the semantics of propositional dependent type theories. PhD thesis, University of Leeds, 2024. https://etheses.whiterose.ac.uk/id/eprint/35802/

    2024

  31. [39]

    Correctness of the Interpretation of the Calculus of Constructions in Doctrines of Constructions, pages 156–220

    T.Streicher. Correctness of the Interpretation of the Calculus of Constructions in Doctrines of Constructions, pages 156–220. Birkhäuser Boston, Boston, MA, 1991

    1991

  32. [40]

    Streicher

    T. Streicher. Semantics of type theory — Correctness, completeness and independence results. Progress in Theoretical Computer Science. Birkhäuser Boston, Inc., Boston, MA, 1991

    1991

  33. [41]

    Streicher

    T. Streicher. The genesis of the groupoid model. Math. Structures Comput. Sci., 31(9):1003–1005, 2021

    2021

  34. [42]

    Taylor.Practical foundations of mathematics, volume 59 ofCambridge Studies in Ad- vanced Mathematics

    P. Taylor.Practical foundations of mathematics, volume 59 ofCambridge Studies in Ad- vanced Mathematics. Cambridge University Press, 1999

    1999

  35. [43]

    van den Berg

    B. van den Berg. Path categories and propositional identity types.ACM Trans. Comput. Log., 19(2):Art. 15, 32, 2018

    2018

  36. [44]

    van den Berg and M

    B. van den Berg and M. den Besten. Quadratic type checking for objective type theory. arXiv e-prints, page arXiv:2102.00905, February 2021

    2021 arXiv

  37. [45]

    van den Berg and I

    B. van den Berg and I. Moerdijk. Exact completion of path categories and algebraic set theory. Part I: Exact completion of path categories.J. Pure Appl. Algebra, 222(10):3137– 3181, 2018

    2018

  38. [46]

    J. Vidmar. Polynomial functors and W-types for groupoids. PhD thesis, University of Leeds, 2018. https://etheses.whiterose.ac.uk/22517/

    2018

  39. [47]

    Winterhalter.Formalisation and meta-theory of type theory

    T. Winterhalter.Formalisation and meta-theory of type theory. PhD thesis, Université de Nantes, 2020. 64

    2020

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.