Document Open Access Logo

Synthetic 1-Categories in Directed Type Theory

Authors Jacob Neumann , Thorsten Altenkirch

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2024.7.pdf
  • Filesize: 0.91 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Semantics
  • directed type theory
  • homotopy type theory
  • category theory
  • generalized algebraic theories

Metrics

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

Abstract

The field of directed type theory seeks to design type theories capable of reasoning synthetically about (higher) categories, by generalizing the symmetric identity types of Martin-Löf Type Theory to asymmetric hom-types. We articulate the directed type theory of the category model, with appropriate modalities for keeping track of variances and a powerful directed-J rule capable of proving results about arbitrary terms of hom-types; we put this rule to use in making several constructions in synthetic 1-category theory. Because this theory is expressed entirely in terms of generalized algebraic theories, we know automatically that this directed type theory admits a syntax model.

Cite As Get BibTex

Jacob Neumann and Thorsten Altenkirch. Synthetic 1-Categories in Directed Type Theory. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.TYPES.2024.7

Author Details

Jacob Neumann
  • University of Nottingham, UK
Thorsten Altenkirch
  • University of Nottingham, UK

Funding

  • Neumann, Jacob: This publication is based upon work from COST Action EuroProofNet, supported by COST (European Cooperation in Science and Technology, www.cost.eu).

References

  1. Benedikt Ahrens, Paige Randall North, and Niels van der Weide. Bicategorical type theory: semantics and syntax. Mathematical Structures in Computer Science, 33(10), 2023. URL: https://doi.org/10.1017/s0960129523000312.
  2. Thorsten Altenkirch. Extensional equality in intensional type theory. In Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pages 412-420. IEEE, 1999. URL: https://doi.org/10.1109/LICS.1999.782636.
  3. Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Christian Sattler, and Filippo Sestini. Constructing a universe for the setoid model. In FoSSaCS, pages 1-21, 2021. URL: https://doi.org/10.1007/978-3-030-71995-1_1.
  4. Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, and Michael Shulman. Internal parametricity, without an interval. Proceedings of the ACM on Programming Languages, 8(POPL):2340-2369, 2024. URL: https://doi.org/10.1145/3632920.
  5. Thorsten Altenkirch, Ambrus Kaposi, and Michael Shulman. Towards higher observational type theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). University of Nantes, 2022. Google Scholar
  6. John C. Baez and Michael Shulman. Lectures on n-categories and cohomology, 2007. URL: https://arxiv.org/abs/math/0608420.
  7. Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M Pitts, and Bas Spitters. Modal dependent type theory and dependent right adjoints. Mathematical Structures in Computer Science, 30(2):118-138, 2020. URL: https://doi.org/10.1017/S0960129519000197.
  8. Rafaël Bocquet. External univalence for second-order generalized algebraic theories. CoRR, abs/2211.07487, 2022. URL: https://doi.org/10.48550/arXiv.2211.07487.
  9. John Cartmell. Generalised algebraic theories and contextual categories. Annals of pure and applied logic, 32:209-243, 1986. URL: https://doi.org/10.1016/0168-0072(86)90053-9.
  10. Simon Castellan, Pierre Clairambault, and Peter Dybjer. Categories with families: Unityped, simply typed, and dependently typed. CoRR, abs/1904.00827:135-180, 2019. URL: https://doi.org/10.48550/arXiv.1904.00827.
  11. Fernando Chu, Éléonore Mangel, and Paige Randall North. A directed homotopy type theory for 1-categories. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). IT University of Copenhagen, 2024. Google Scholar
  12. Peter Dybjer. Internal type theory. In International Workshop on Types for Proofs and Programs, pages 120-134. Springer, 1995. URL: https://doi.org/10.1007/3-540-61780-9_66.
  13. Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal. Multimodal dependent type theory. 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 492-506. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394736.
  14. Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. The yoneda embedding in simplicial type theory, 2025. URL: https://doi.org/10.48550/arXiv.2501.13229.
  15. Martin Hofmann. A simple model for quotient types. In International Conference on Typed Lambda Calculi and Applications, pages 216-234. Springer, 1995. URL: https://doi.org/10.1007/BFb0014055.
  16. Martin Hofmann. Syntax and semantics of dependent types. In Extensional Constructs in Intensional Type Theory, pages 13-54. Springer, 1997. Google Scholar
  17. Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. Twenty-five years of constructive type theory (Venice, 1995), 36:83-111, 1995. Google Scholar
  18. Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing quotient inductive-inductive types. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290315.
  19. Ambrus Kaposi and Szumi Xie. Second-order generalised algebraic theories: Signatures and first-order semantics. In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia, volume 299 of LIPIcs, pages 10:1-10:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.FSCD.2024.10.
  20. András Kovács. Type-Theoretic Signatures for Algebraic Theories and Inductive Types. PhD thesis, Eötvös Loránd University, 2022. Google Scholar
  21. Nikolai Kudasov, Emily Riehl, and Jonathan Weinberger. Formalizing the ∞-categorical yoneda lemma, 2023. URL: https://doi.org/10.48550/arXiv.2309.08340.
  22. Daniel R. Licata and Robert Harper. 2-dimensional directed type theory. In Michael W. Mislove and Joël Ouaknine, editors, Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011, Pittsburgh, PA, USA, May 25-28, 2011, volume 276 of Electronic Notes in Theoretical Computer Science, pages 263-289. Elsevier, 2011. URL: https://doi.org/10.1016/j.entcs.2011.09.026.
  23. Per Martin-Löf. An intuitionistic theory of types: Predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. Elsevier, 1975. Google Scholar
  24. Per Martin-Löf. Constructive mathematics and computer programming. In L. Jonathan Cohen, Jerzy Łoś, Helmut Pfeiffer, and Klaus-Peter Podewski, editors, Logic, Methodology and Philosophy of Science VI, volume 104 of Studies in Logic and the Foundations of Mathematics, pages 153-175. Elsevier, 1982. Google Scholar
  25. Jacob Neumann. A Generalized Algebraic Theory of Directed Equality. PhD thesis, University of Nottingham, 2025. Google Scholar
  26. Jacob Neumann and Thorsten Altenkirch. Synthetic 1-categories in directed type theory. CoRR, abs/2410.19520, 2024. URL: https://doi.org/10.48550/arXiv.2410.19520.
  27. Max S. New and Daniel R. Licata. A formal logic for formal category theory. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, volume 13992 of Lecture Notes in Computer Science, pages 113-134. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_6.
  28. Paige Randall North. Towards a directed homotopy type theory. Electronic Notes in Theoretical Computer Science, 347:223-239, 2019. URL: https://doi.org/10.1016/j.entcs.2019.09.012.
  29. Andreas Nuyts. Towards a directed homotopy type theory based on 4 kinds of variance. Mém. de mast. Katholieke Universiteit Leuven, 2015. Google Scholar
  30. E. Riehl and M. Shulman. A type theory for synthetic ∞-categories. Higher Structures, 1(1):116-193, 2017. URL: https://doi.org/10.2140/hs.2017.1.116.
  31. Michael Shulman. Towards a third-generation HOTT, 2022. Carnegie Mellon University HoTT Seminar. URL: https://www.cmu.edu/dietrich/philosophy/hott/seminars/index.html.
  32. Taichi Uemura. Abstract and concrete type theories. PhD thesis, University of Amsterdam, 2021. Google Scholar
  33. Taichi Uemura. A general framework for the semantics of type theory. Mathematical Structures in Computer Science, 33(3), March 2023. URL: https://doi.org/10.1017/s0960129523000208.
  34. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book.
  35. Benno Van Den Berg and Richard Garner. Types are weak ω-groupoids. Proceedings of the london mathematical society, 102(2):370-394, 2011. Google Scholar
  36. Matthew Z. Weaver and Daniel R. Licata. A constructive model of directed univalence in bicubical sets. 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, LICS '20, pages 915-928, New York, NY, USA, 2020. ACM. URL: https://doi.org/10.1145/3373718.3394794.
  37. Jonathan Weinberger and Ulrik Buchholtz. Type-theoretic modalities for synthetic (∞,1)-categories, 2019. International Conference on Homotopy Type Theory (HoTT 2019). Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact