Document Open Access Logo

Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses

Author Taichi Uemura

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2023.5.pdf
  • Filesize: 0.85 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Denotational semantics
  • Theory of computation → Categorical semantics
Keywords
  • Homotopy type theory
  • ∞-logos
  • ∞-topos
  • oplax limit
  • Artin gluing
  • modality
  • synthetic Tait computability
  • logical relation

Metrics

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

Abstract

We show that certain diagrams of ∞-logoses are reconstructed in internal languages of their oplax limits via lex, accessible modalities, which enables us to use plain homotopy type theory to reason about not only a single ∞-logos but also a diagram of ∞-logoses. This also provides a higher dimensional version of Sterling’s synthetic Tait computability - a type theory for higher dimensional logical relations.

Cite As Get BibTex

Taichi Uemura. Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.FSCD.2023.5

Author Details

Taichi Uemura
  • Stockholm University, Sweden

Funding

  • Uemura, Taichi: Supported by KAW Grant "Type Theory for Mathematics and Computer Science" investigated by Thierry Coquand and Peter LeFanu Lumsdaine.

Acknowledgements

The author thanks Jonathan Sterling for useful conversations on the current work. The author also thanks anonymous referees for corrections, comments, and suggestions.

References

  1. Mathieu Anel, Georg Biedermann, Eric Finster, and André Joyal. A generalized Blakers-Massey theorem. J. Topol., 13(4):1521-1553, 2020. URL: https://doi.org/10.1112/topo.12163.
  2. Mathieu Anel and André Joyal. Topo-logie. In New spaces in mathematics. Formal and conceptual reflections, pages 155-257. Cambridge University Press, 2021. URL: https://doi.org/10.1017/9781108854429.007.
  3. Peter Arndt and Krzysztof Kapulkin. Homotopy-Theoretic Models of Type Theory. In Luke Ong, editor, Typed Lambda Calculi and Applications: 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings, pages 45-60, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-21691-6_7.
  4. Steve Awodey and Michael A. Warren. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146(1):45-55, 2009. URL: https://doi.org/10.1017/S0305004108001783.
  5. Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Proofs for Free: Parametricity for Dependent Types. Journal of Functional Programming, 22(2):107-152, March 2012. URL: https://doi.org/10.1017/S0956796812000056.
  6. John W. Duskin. Simplicial matrices and the nerves of weak n-categories. I. Nerves of bicategories. Theory Appl. Categ., 9:198-308, 2001/02. CT2000 Conference (Como). URL: http://www.tac.mta.ca/tac/volumes/9/n10/9-10abs.html.
  7. Eric Finster. A Note on Left Exact Modalities in Type Theory. URL: https://ericfinster.github.io/files/lmhtt.pdf.
  8. Daniel Gratzer. Normalization for Multimodal Type Theory. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 2:1-2:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3532398.
  9. Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal. Multimodal Dependent Type Theory. Logical Methods in Computer Science, Volume 17, Issue 3, July 2021. URL: https://doi.org/10.46298/lmcs-17(3:11)2021.
  10. Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, and Peter LeFanu Lumsdaine. A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 565-574, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2933575.2934545.
  11. Peter T. Johnstone. Sketches of an Elephant : A Topos Theory Compendium Volume 1, volume 43 of Oxford Logic Guides. Oxford University Press, 2002. Google Scholar
  12. Marc Lasson. Canonicity of Weak ω-groupoid Laws Using Parametricity Theory. Electronic Notes in Theoretical Computer Science, 308:229-244, 2014. URL: https://doi.org/10.1016/j.entcs.2014.10.013.
  13. F. William Lawvere. Axiomatic cohesion. Theory Appl. Categ., 19:No. 3, 41-49, 2007. URL: http://www.tac.mta.ca/tac/volumes/19/3/19-03abs.html.
  14. Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal Universes in Models of Homotopy Type Theory. In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), volume 108 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:17, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.22.
  15. Peter LeFanu Lumsdaine and Michael A. Warren. The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories. ACM Trans. Comput. Logic, 16(3):23:1-23:31, July 2015. URL: https://doi.org/10.1145/2754931.
  16. Jacob Lurie. Higher Topos Theory, volume 170 of Annals of Mathematics Studies. Princeton University Press, 2009. URL: https://www.math.ias.edu/~lurie/papers/HTT.pdf.
  17. Jacob Lurie. (∞,2)-Categories and the Goodwillie Calculus I, 2009. URL: https://arxiv.org/abs/0905.0462v2.
  18. Michael Makkai. First Order Logic with Dependent Sorts, with Applications to Category Theory, 1995. URL: http://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf.
  19. Per Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. Studies in Logic and the Foundations of Mathematics, 80:73-118, 1975. URL: https://doi.org/10.1016/S0049-237X(08)71945-1.
  20. Hoang Kim Nguyen and Taichi Uemura. ∞-type theories, 2022. URL: https://arxiv.org/abs/2205.00798v1.
  21. Egbert Rijke. Introduction to Homotopy Type Theory, 2022. URL: https://arxiv.org/abs/2212.11082v1.
  22. Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Log. Methods Comput. Sci., 16(1):Paper No. 2, 79, 2020. URL: https://doi.org/10.23638/LMCS-16(1:2)2020.
  23. Urs Schreiber and Michael Shulman. Quantum Gauge Field Theory in Cohesive Homotopy Type Theory. In Ross Duncan and Prakash Panangaden, editors, Proceedings 9th Workshop on Quantum Physics and Logic, QPL 2012, Brussels, Belgium, 10-12 October 2012, volume 158 of EPTCS, pages 109-126, 2012. URL: https://doi.org/10.4204/EPTCS.158.8.
  24. Michael Shulman. Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science, 25(05):1203-1277, 2015. URL: https://doi.org/10.1017/s0960129514000565.
  25. Michael Shulman. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science, 28(6):856-941, 2018. URL: https://doi.org/10.1017/S0960129517000147.
  26. Michael Shulman. All (∞,1)-toposes have strict univalent universes, 2019. URL: https://arxiv.org/abs/1904.07004v2.
  27. Jonathan Sterling. First Steps in Synthetic Tait Computability. PhD thesis, Carnegie Mellon University, 2021. URL: https://www.jonmsterling.com/pdfs/sterling:2021:thesis.pdf.
  28. Jonathan Sterling and Carlo Angiuli. Normalization for Cubical Type Theory. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-15, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470719.
  29. Jonathan Sterling and Robert Harper. Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. J. ACM, 68(6):41:1-41:47, 2021. URL: https://doi.org/10.1145/3474834.
  30. Jonathan Sterling and Robert Harper. Sheaf Semantics of Termination-Insensitive Noninterference. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:19, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.5.
  31. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics, 2013. URL: http://homotopytypetheory.org/book/.
  32. Taichi Uemura. Fibred Fibration Categories. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12, June 2017. URL: https://doi.org/10.1109/LICS.2017.8005084.
  33. Taichi Uemura. Homotopy type theory as internal languages of diagrams of ∞-logoses, 2022. URL: https://arxiv.org/abs/2212.02444v1.
  34. Taichi Uemura. Normalization and coherence for ∞-type theories, 2022. URL: https://arxiv.org/abs/2212.11764v1.
  35. Gavin Wraith. Artin glueing. J. Pure Appl. Algebra, 4:345-348, 1974. URL: https://doi.org/10.1016/0022-4049(74)90014-0.
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