Document Open Access Logo

The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories

Authors Daniël Otten , Matteo Spadetto

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.38.pdf
  • Filesize: 1.69 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Categorical semantics
  • Mathematics of computing → Topology
Keywords
  • Axiomatic type theory
  • cubical type theory
  • propositional equality
  • biequivalence
  • display map categories
  • path categories
  • homotopy theory
  • coherence

Metrics

Abstract

The semantics of extensional type theory has an elegant categorical description: models of extensional =-types, 𝟙-types, and Σ-types are biequivalent to finitely complete categories, while adding Π-types yields locally Cartesian closed categories. We establish parallel results for axiomatic type theory, which includes systems like cubical type theory, where the computation rule of the =-types only holds as a propositional axiom instead of a definitional reduction. In particular, we prove that models of axiomatic =-types, and standard 𝟙- and Σ-types are biequivalent to certain path categories, while adding axiomatic Π-types yields dependent homotopy exponents.
This biequivalence simplifies axiomatic =-types, which are more intricate than extensional ones since they permit higher dimensional structure. Specifically, path categories use a primitive notion of equivalence instead of a direct reproduction of the syntactic elimination rules and computation axioms. We apply our correspondence to prove a coherence theorem: we show that these weak homotopical models can be turned into equivalent strict models of axiomatic type theory. In addition, we introduce a more modular notion, that of a display map path category, which only models axiomatic =-types by default, while leaving room to add other axiomatic type formers such as 𝟙-, Σ-, and Π-types.

Cite As Get BibTex

Daniël Otten and Matteo Spadetto. The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 38:1-38:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.38

Author Details

Daniël Otten
  • ILLC, University of Amsterdam, The Netherlands
Matteo Spadetto
  • DMIF, University of Udine, Italy
  • LS2N, University of Nantes, France

Funding

  • Otten, Daniël: This publication is part of the project "The Power of Equality" (with project number OCENW.M20.380) of the research programme Open Competition Science M 2 which is (partly) financed by the Dutch Research Council (NWO).
  • Spadetto, Matteo: The author was supported by an E-COST-CA20111 Short-Term Scientific Mission Grant - that funded his research visit to Amsterdam in Spring 2023, where and when this research started - a School of Mathematics full-time EPSRC Doctoral Training Partnership Studentship 2019/2020, the Italian MUR PRIN 2022 "STENDHAL", and eOTP RECIPROG.

Acknowledgements

We are thankful to Benno van den Berg, Rafaël Bocquet, Jacopo Emmenegger, Ambrus Kaposi, Marino Miculan, and Niels van der Weide for many helpful discussions and ideas.

References

  1. B. Ahrens, P. Lumsdaine, and P. Randall North. Comparing semantic frameworks for dependently-sorted algebraic theories. In Oleg Kiselyov, editor, Programming Languages and Systems, volume 15194 of Lecture Notes in Computer Science, pages 3-22, Singapore, 2025. Springer Nature Singapore. URL: https://doi.org/10.1007/978-981-97-8943-6_1.
  2. T. Altenkirch, P. Capriotti, and N. Kraus. Extending Homotopy Type Theory with Strict Equality. LIPIcs, Volume 62, CSL 2016, 62:21:1-21:17, 2016. arXiv:1604.03799 [cs]. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.21.
  3. 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. URL: https://doi.org/10.1109/LICS.2012.21.
  4. S. Awodey, N. Gambino, and K. Sojakova. Homotopy-initial algebras in type theory. J. ACM, 63(6):Art. 51, 45, 2017. URL: https://doi.org/10.1145/3006383.
  5. S. Awodey and M. A. Warren. Homotopy theoretic models of identity types. Math. Proc. Cambridge Philos. Soc., 146(1):45-55, 2009. URL: https://doi.org/10.1017/S0305004108001783.
  6. B. van den Berg. Path categories and propositional identity types. ACM Trans. Comput. Log., 19(2):Art. 15, 32, 2018. URL: https://doi.org/10.1145/3204492.
  7. B. van den Berg. Univalent polymorphism. Annals of Pure and Applied Logic, 171(6):102793, June 2020. URL: https://doi.org/10.1016/j.apal.2020.102793.
  8. B. van den Berg and M. den Besten. Quadratic type checking for objective type theory, 2021. URL: https://arxiv.org/abs/2102.00905.
  9. 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. URL: https://doi.org/10.1016/j.jpaa.2017.11.017.
  10. M. den Besten. On homotopy exponentials in path categories, 2020. URL: https://arxiv.org/abs/2010.14313.
  11. R. Bocquet. Coherence of strict equalities in dependent type theories, 2020. URL: https://arxiv.org/abs/2010.14166.
  12. R. Bocquet. Strictification of weakly stable type-theoretic structures using generic contexts. In 27th International Conference on Types for Proofs and Programs, volume 239 of LIPIcs. Leibniz Int. Proc. Inform., pages Art. No. 3, 23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/lipics.types.2021.3.
  13. S. Boulier and T. Winterhalter. Weak type theory is rather strong. 30th International Conference on Types for Proofs and Programs, 2019. URL: https://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_18.
  14. K. S. Brown. Abstract homotopy theory and generalized sheaf cohomology. Transactions of the American Mathematical Society, 186:419-458, 1973. Google Scholar
  15. J. Cartmell. Generalised Algebraic Theories and Contextual Categories. PhD thesis, University of Oxford, 1978. Google Scholar
  16. P. Clairambault and P. Dybjer. The biequivalence of locally cartesian closed categories and Martin-Löf type theories. Math. Structures Comput. Sci., 24(6):e240606, 54, 2014. URL: https://doi.org/10.1017/S0960129513000881.
  17. J. Cockx. Type theory unchained: Extending agda with user-defined rewrite rules. In 25th International Conference on Types for Proofs and Programs (TYPES 2019), volume 175 of Leibniz International Proceedings in Informatics (LIPIcs), pages 2:1-2:27. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.TYPES.2019.2.
  18. C. Cohen, T. Coquand, S. Huber, and A. Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:34. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2018. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  19. P.-L. Curien. Substitution up to isomorphism. Fundamenta Informaticae, 19(1-2):51-85, 1993. Google Scholar
  20. P.-L. Curien, R. Garner, and M. Hofmann. Revisiting the categorical interpretation of dependent type theory. Theoretical Computer Science, 546:99-119, 2014. Models of Interaction: Essays in Honour of Glynn Winskel. URL: https://doi.org/10.1016/j.tcs.2014.03.003.
  21. N. Gambino and R. Garner. The identity type weak factorisation system. Theoretical Computer Science, 409(1):94-109, 2008. URL: https://doi.org/10.1016/j.tcs.2008.08.030.
  22. N. Gambino and M. F. Larrea. Models of Martin-Löf type theory from algebraic weak factorisation systems. J. Symb. Log., 88(1):242-289, 2023. URL: https://doi.org/10.1017/jsl.2021.39.
  23. R. Garner. On the strength of dependent products in the type theory of Martin-Löf. Annals of Pure and Applied Logic, 160(1):1-12, 2009. Publisher: Elsevier. URL: https://doi.org/10.1016/J.APAL.2008.12.003.
  24. R. Garner. Two-dimensional models of type theory. Math. Structures Comput. Sci., 19(4):687-736, 2009. URL: https://doi.org/10.1017/S0960129509007646.
  25. R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. J. ACM, 40(1):143-184, 1993. URL: https://doi.org/10.1145/138027.138060.
  26. 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. Google Scholar
  27. M. Hofmann. Syntax and semantics of dependent types, pages 13-54. Springer, London, 1997. URL: https://doi.org/10.1007/978-1-4471-0963-1_2.
  28. J. Hyland, E. Martin, and A. Pitts. The theory of constructions: Categorical semantics and topos-theoretic models. Categories in Computer Science and Logic, 92:137-199, 1989. Google Scholar
  29. B. Jacobs. Comprehension categories and the semantics of type dependency. Theoret. Comput. Sci., 107(2):169-207, 1993. URL: https://doi.org/10.1016/0304-3975(93)90169-T.
  30. A. Joyal. Notes on clans and tribes, 2017. URL: https://arxiv.org/abs/1710.10238.
  31. A. Kaposi and L. Pujet. Type theory in type theory using a strictified syntax, 2025. URL: https://pujet.fr/pdf/strictification_preprint.pdf.
  32. P. L. Lumsdaine. Strong functional extensionality from weak, 2011. URL: https://homotopytypetheory.org/2011/12/19/strong-funext-from-weak/.
  33. 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. URL: https://doi.org/10.1145/2754931.
  34. M. E. Maietti. Modular correspondence between dependent type theories and categories including pretopoi and topoi. Math. Structures Comput. Sci., 15(6):1089-1149, 2005. URL: https://doi.org/10.1017/S0960129505004962.
  35. M. E. Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3):319-354, 2009. Computation and Logic in the Real World: CiE 2007. URL: https://doi.org/10.1016/j.apal.2009.01.006.
  36. P. Martin-Löf. Constructive mathematics and computer programming. In Studies in Logic and the Foundations of Mathematics, volume 104, pages 153-175. Elsevier, 1982. Google Scholar
  37. P. Martin-Löf. Intuitionistic type theory, volume 1 of Studies in Proof Theory. Lecture Notes. Bibliopolis, Naples, 1984. Notes by Giovanni Sambin. Google Scholar
  38. E. Moggi. A category-theoretic account of program modules. Math. Structures Comput. Sci., 1(1):103-139, 1991. URL: https://doi.org/10.1017/S0960129500000074.
  39. D. Otten and M. Spadetto. The biequivalence of path categories and axiomatic Martin-Löf type theories (full version), 2025. URL: https://arxiv.org/abs/2503.15431.
  40. E. Paauw. Path categories and ∞-groupoids. Master’s thesis, University of Amsterdam, 2021. URL: https://scripties.uba.uva.nl/search?id=record_29430.
  41. C. Paulin-Mohring. Inductive definitions in the system coq rules and properties. In International Conference on Typed Lambda Calculi and Applications, pages 328-345. Springer, 1993. Google Scholar
  42. A. Radulescu-Banu. Cofibrations in homotopy theory, 2009. URL: https://arxiv.org/abs/math/0610009.
  43. R. A. G. Seely. Locally Cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc., 95(1):33-48, 1984. URL: https://doi.org/10.1017/S0305004100061284.
  44. M. Spadetto. A 2-categorical approach to the semantics of dependent type theory with computation axioms, 2025. URL: https://arxiv.org/abs/2507.07208.
  45. M. Spadetto. Relating homotopy equivalences to conservativity in dependent type theories with computation axioms. Logical Methods in Computer Science, Volume 21, Issue 3, September 2025. URL: https://doi.org/10.46298/lmcs-21(3:32)2025.
  46. P. Taylor. Practical foundations of mathematics, volume 59 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999. Google Scholar
  47. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  48. N. van der Weide. The internal languages of univalent categories. In 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 112-126, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00016.
  49. T. Winterhalter. Formalisation and meta-theory of type theory. PhD thesis, Université de Nantes, 2020. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact