Document Open Access Logo

Formalisation of Dependent Type Theory: The Example of CaTT

Author Thibaut Benjamin

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2021.2.pdf
  • Filesize: 0.83 MB
  • 21 pages

Document Identifiers

Author Details

Thibaut Benjamin
  • Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France

Acknowledgements

I want to thank Samuel Mimram and Eric Finster for their guidance in this project and the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Thibaut Benjamin. Formalisation of Dependent Type Theory: The Example of CaTT. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.TYPES.2021.2

Abstract

We present the type theory CaTT, originally introduced by Finster and Mimram to describe globular weak ω-categories, formalise this theory in the language of homotopy type theory and discuss connections with the open problem internalising higher structures. Most of the studies about this type theory assume that it is well-formed and satisfy the usual syntactic properties that dependent type theories enjoy, without being completely clear and thorough about what these properties are exactly. We use our formalisation to list and formally prove all of these meta-properties, thus filling a gap in the foundational aspect. We discuss the aspects of the formalisation inherent to CaTT. We present the formalisation in a way that not only handles the type theory CaTT but also related type theories that share the same structure, and in particular we show that this formalisation provides a proper ground to the study of the theory MCaTT which describes the globular monoidal weak ω-categories. The article is accompanied by a development in the proof assistant Agda to check the formalisation that we present.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Categorical semantics
Keywords
  • Dependent type theory
  • homotopy type theory
  • higher categories
  • formalisation
  • Agda
  • proof assistant

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Andreas Abel, Joakim Öhman, and Andrea Vezzosi. Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158111.
  2. Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Extending homotopy type theory with strict equality. CoRR, 2016. URL: http://arxiv.org/abs/1604.03799.
  3. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. ACM SIGPLAN Notices, 51(1):18-29, 2016. URL: https://doi.org/10.1145/2837614.2837638.
  4. Thorsten Altenkirch and Ondrej Rypacek. A syntactical approach to weak omega-groupoids. In 26th Computer Science Logic (CSL'12), volume 16 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.16.
  5. Michael A Batanin. Monoidal globular categories as a natural environment for the theory of weak n-categories. Advances in Mathematics, 136(1):39-103, 1998. URL: https://doi.org/10.1006/aima.1998.1724.
  6. Andrej Bauer, Philipp G Haselwarter, and Peter LeFanu Lumsdaine. A general definition of dependent type theories. CoRR, 2020. URL: http://arxiv.org/abs/2009.05539.
  7. Thibaut Benjamin. A type theoretic approach to weak ω-categories and related higher structures. PhD thesis, Institut Polytechnique de Paris, 2020. Google Scholar
  8. Thibaut Benjamin. Monoidal weak ω-categories as models of a type theory. CoRR, abs/2111.14208, 2021. URL: http://arxiv.org/abs/2111.14208.
  9. Thibaut Benjamin, Eric Finster, and Samuel Mimram. Globular weak ω-categories as models of a type theory. CoRR, 2021. URL: http://arxiv.org/abs/2106.04475.
  10. Thibaut Benjamin and Samuel Mimram. Suspension et Fonctorialité: Deux Opérations Implicites Utiles en CaTT. In Journées Francophones des Langages Applicatifs, 2019. Google Scholar
  11. James Chapman. Type theory should eat itself. Electronic notes in theoretical computer science, 228:21-36, 2009. URL: https://doi.org/10.1016/j.entcs.2008.12.114.
  12. Peter Dybjer. Internal Type Theory. In Types for Proofs and Programs. TYPES 1995, pages 120-134. Springer, Berlin, Heidelberg, 1996. URL: https://doi.org/10.1007/3-540-61780-9_66.
  13. Eric Finster and Samuel Mimram. A Type-Theoretical Definition of Weak ω-Categories. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005124.
  14. Alexander Grothendieck. Pursuing stacks. Unpublished manuscript, 1983. Google Scholar
  15. Hakon Gylterud. Defining and relating theories. Presentation HoTT Electronic Seminar, 2021. Google Scholar
  16. Hugo Herbelin. A dependently-typed construction of semi-simplicial types. Mathematical Structures in Computer Science, 25(5):1116-1131, 2015. URL: https://doi.org/10.1017/S0960129514000528.
  17. Ambrus Kaposi, András Kovács, and Ambroise Lafont. For finitary induction-induction, induction is enough. In TYPES 2019, volume 175 of LIPIcs, pages 6:1-6:30. Schloss Dagstuhl-Leibniz-Zentrum für Informatik GmbH, 2020. URL: https://doi.org/10.4230/LIPIcs.TYPES.2019.6.
  18. Nicolai Kraus. Internal ∞-categorical models of dependent type theory: Towards 2ltt eating hott. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470667.
  19. Ambroise Lafont, Tom Hirschowitz, and Nicolas Tabareau. Types are weak omega-groupoids, in Coq. TYPES 2018, 2018. Google Scholar
  20. Chaitanya Leena-Subramaniam. From dependent type theory to higher algebraic structures. PhD thesis, Université Paris 7, 2021. URL: http://arxiv.org/abs/2110.02804.
  21. Peter LeFanu Lumsdaine. Weak ω-categories from intensional type theory. In TLCA, pages 172-187. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02273-9_14.
  22. Georges Maltsiniotis. Grothendieck ∞-groupoids, and still another definition of ∞-categories. CoRR, 2010. URL: http://arxiv.org/abs/1009.2331.
  23. Hoang Kim Nguyen and Taichi Uemura. ∞-type theories. In abstract presented at the online workshop HoTT/UF’20, 2020. Google Scholar
  24. Mike Shulman. Homotopy type theory should eat itself (but so far, it’s too big to swallow), 2014. URL: https://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/.
  25. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. The MetaCoq project. Journal of Automated Reasoning, 64(5):947-999, 2020. URL: https://doi.org/10.1007/s10817-019-09540-0.
  26. Taichi Uemura. A general framework for the semantics of type theory. CoRR, 2019. URL: http://arxiv.org/abs/1904.04097.
  27. Benno Van Den Berg and Richard Garner. Types are weak ω-groupoids. Proceedings of the London Mathematical Society, 102(2):370-394, 2011. URL: https://doi.org/10.1112/plms/pdq026.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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