Document Open Access Logo

The Groupoid-Syntax of Type Theory Is a Set

Authors Thorsten Altenkirch , Ambrus Kaposi , Szumi Xie

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.40.pdf
  • Filesize: 1.85 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Categorical models of type theory
  • category with families
  • groupoids
  • coherence
  • homotopy type theory

Metrics

Abstract

Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, we introduce the concept of a Groupoid Category with Families (GCwF). This framework truncates types at the groupoid level and incorporates coherence equations, providing a natural extension of the CwF framework when starting from a 1-category.
We demonstrate that the initial GCwF for a type theory with a base family of sets and Π-types (groupoid-syntax) is set-truncated. Consequently, this allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models. All constructions in this paper were formalised in Cubical Agda.

Cite As Get BibTex

Thorsten Altenkirch, Ambrus Kaposi, and Szumi Xie. The Groupoid-Syntax of Type Theory Is a Set. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 40:1-40:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.40

Author Details

Thorsten Altenkirch
  • University of Nottingham, UK
Ambrus Kaposi
  • Eötvös Loránd University (ELTE), Budapest, Hungary
Szumi Xie
  • Eötvös Loránd University (ELTE), Budapest, Hungary

Funding

The first author was supported by project no. TKP2021-NVA-29 which has been implemented with the support provided by the Ministry of Culture and Innovation of Hungary from the National Research, Development and Innovation Fund, financed under the TKP2021-NVA funding scheme. The second and third authors were funded by the European Union (ERC, HOTT, 101170308). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.

Acknowledgements

We thank the reviewers for their helpful comments and suggestions. We thank Niels van der Weide for explaining us the relationship to comprehension categories.

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):23:1-23:29, 2018. URL: https://doi.org/10.1145/3158111.
  2. Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, and Loïc Pujet. Martin-Löf à la Coq. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 230-245. ACM, 2024. URL: https://doi.org/10.1145/3636501.3636951.
  3. Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Extending homotopy type theory with strict equality. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 21:1-21:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.21.
  4. Thorsten Altenkirch, Nils Anders Danielsson, and Nicolai Kraus. Partiality, revisited - the partiality monad as a quotient inductive-inductive type. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 534-549, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_31.
  5. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 18-29. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837638.
  6. Thorsten Altenkirch and Ambrus Kaposi. Normalisation by evaluation for type theory, in type theory. Logical methods in computer science, 13, 2017. URL: https://doi.org/10.23638/LMCS-13(4:1)2017.
  7. Thorsten Altenkirch and Ambrus Kaposi. A container model of type theory. In Henning Basold, editor, 27th International Conference on Types for Proofs and Programs, TYPES 2021. Universiteit Leiden, 2021. URL: https://types21.liacs.nl/download/a-container-model-of-type-theory/.
  8. Thorsten Altenkirch and Luis Scoccola. The integers as a higher inductive type. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 67-73. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394760.
  9. Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications. Math. Struct. Comput. Sci., 33(8):688-743, 2023. URL: https://doi.org/10.1017/S0960129523000130.
  10. Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications - ERRATUM. Math. Struct. Comput. Sci., 34(1):80, 2024. URL: https://doi.org/10.1017/S096012952300021X.
  11. Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson. Symmetry. https://github.com/UniMath/SymmetryBook. Commit: ec9be72.
  12. Rafaël Bocquet. Strictification of weakly stable type-theoretic structures using generic contexts. In Henning Basold, Jesper Cockx, and Silvia Ghilezan, editors, 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference), volume 239 of LIPIcs, pages 3:1-3:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.TYPES.2021.3.
  13. Simon Castellan, Pierre Clairambault, and Peter Dybjer. Categories with Families: Unityped, Simply Typed, and Dependently Typed, pages 135-180. Springer International Publishing, Cham, 2021. URL: https://doi.org/10.1007/978-3-030-66545-6_5.
  14. Evan Cavallo and Robert Harper. Higher inductive types in cubical computational type theory. Proc. ACM Program. Lang., 3(POPL):1:1-1:27, 2019. URL: https://doi.org/10.1145/3290314.
  15. James Chapman. Type theory should eat itself. In Andreas Abel and Christian Urban, editors, Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008, volume 228 of Electronic Notes in Theoretical Computer Science, pages 21-36. Elsevier, 2008. URL: https://doi.org/10.1016/J.ENTCS.2008.12.114.
  16. Pierre Clairambault and Peter Dybjer. The biequivalence of locally cartesian closed categories and martin-löf type theories. Math. Struct. Comput. Sci., 24(6), 2014. URL: https://doi.org/10.1017/S0960129513000881.
  17. Thierry Coquand. Generalised algebraic presentation of type theory, 2020. URL: https://www.cse.chalmers.se/~coquand/cwf2.pdf.
  18. Thierry Coquand, Simon Huber, and Anders Mörtberg. On higher inductive types in cubical type theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 255-264. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209197.
  19. Nils Anders Danielsson. A formalisation of a dependently typed language as an inductive-recursive family. In Thorsten Altenkirch and Conor McBride, editors, Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, volume 4502 of Lecture Notes in Computer Science, pages 93-109. Springer, 2006. URL: https://doi.org/10.1007/978-3-540-74464-1_7.
  20. Tim Lukas Diezel and Sergey Goncharov. Towards constructive hybrid semantics. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 24:1-24:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.24.
  21. Peter Dybjer. Internal type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers, volume 1158 of Lecture Notes in Computer Science, pages 120-134. Springer, 1995. URL: https://doi.org/10.1007/3-540-61780-9_66.
  22. Thomas Ehrhard. Une sémantique catégorique des types dépendents. PhD thesis, Université Paris VII, 1988. Google Scholar
  23. Martin Hofmann. On the interpretation of type theory in locally cartesian closed categories. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 427-441. Springer, 1994. URL: https://doi.org/10.1007/BFB0022273.
  24. Ambrus Kaposi. Re: Separate definition of constructors?, May 2019. Email message to the Agda mailing list. URL: https://lists.chalmers.se/pipermail/agda/2019/011176.html.
  25. Ambrus Kaposi and András Kovács. Signatures and induction principles for higher inductive-inductive types. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:10)2020.
  26. Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing quotient inductive-inductive types. Proc. ACM Program. Lang., 3(POPL):2:1-2:24, 2019. URL: https://doi.org/10.1145/3290315.
  27. Ambrus Kaposi and Jakob von Raumer. A syntax for mutual inductive families. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 23:1-23:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.23.
  28. G. M. Kelly. On MacLane’s conditions for coherence of natural associativities, commutativities, etc. Journal of Algebra, 1(4):397-402, 1964. URL: https://doi.org/10.1016/0021-8693(64)90018-3.
  29. 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 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470667.
  30. Nicolai Kraus and Thorsten Altenkirch. Free higher groups in homotopy type theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 599-608. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209183.
  31. Peter LeFanu Lumsdaine and Michael A. Warren. The local universes model: An overlooked coherence construction for dependent type theories. ACM Trans. Comput. Log., 16(3):23:1-23:31, 2015. URL: https://doi.org/10.1145/2754931.
  32. Stefano Piceghello. Coherence for monoidal groupoids in HoTT. In Marc Bezem and Assia Mahboubi, editors, 25th International Conference on Types for Proofs and Programs (TYPES 2019), volume 175 of Leibniz International Proceedings in Informatics (LIPIcs), pages 8:1-8:20, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2019.8.
  33. Christian Sattler. Semantics of signatures for higher inductive-inductive types (HIITs) in complete Segal types, 2019. Notes on the author’s website. URL: https://www.cse.chalmers.se/~sattler/docs/hits.
  34. Mike Shulman. Homotopy type theory should eat itself (but so far, it’s too big to swallow), 2014. Blog post on the Homotopy Type Theory website. URL: https://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/.
  35. Taichi Uemura. Normalization and coherence for ∞-type theories. CoRR, abs/2212.11764, 2022. URL: https://doi.org/10.48550/arXiv.2212.11764.
  36. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  37. Niels van der Weide. The internal languages of univalent categories. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025, pages 112-126. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00016.
  38. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. J. Funct. Program., 31:e8, 2021. URL: https://doi.org/10.1017/S0956796821000034.
  39. Vladimir Voevodsky. A C-system defined by a universe category, 2015. URL: https://arxiv.org/abs/1409.7925.
  40. David Wärn. Path spaces of pushouts, 2024. URL: https://arxiv.org/abs/2402.12339.
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