Document Open Access Logo

Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts

Author Rafaël Bocquet

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2021.3.pdf
  • Filesize: 0.49 MB
  • 23 pages

Document Identifiers

Author Details

Rafaël Bocquet
  • Eötvös Loránd University, Budapest, Hungary

Cite AsGet BibTex

Rafaël Bocquet. Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 3:1-3:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.TYPES.2021.3

Abstract

We present a new strictification method for type-theoretic structures that are only weakly stable under substitution. Given weakly stable structures over some model of type theory, we construct equivalent strictly stable structures by evaluating the weakly stable structures at generic contexts. These generic contexts are specified using the categorical notion of familial representability. This generalizes the local universes method of Lumsdaine and Warren. We show that generic contexts can also be constructed in any category with families which is freely generated by collections of types and terms, without any definitional equality. This relies on the fact that they support first-order unification. These free models can only be equipped with weak type-theoretic structures, whose computation rules are given by typal equalities. Our main result is that any model of type theory with weakly stable weak type-theoretic structures admits an equivalent model with strictly stable weak type-theoretic structures.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • type theory
  • strictification
  • coherence
  • familial representability
  • unification

Metrics

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

References

  1. 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.
  2. Martin E. Bidlingmaier. An interpretation of dependent type theory in a model category of locally cartesian closed categories. CoRR, abs/2007.02900, 2020. URL: http://arxiv.org/abs/2007.02900.
  3. Rafaël Bocquet. Coherence of strict equalities in dependent type theories. CoRR, abs/2010.14166, 2020. URL: http://arxiv.org/abs/2010.14166.
  4. Aurelio Carboni and Peter Johnstone. Connected limits, familial representability and artin glueing. Mathematical Structures in Computer Science, 5(4):441-459, 1995. URL: https://doi.org/10.1017/S0960129500001183.
  5. Aurelio Carboni and Peter Johnstone. Corrigenda for ‘connected limits, familial representability and artin glueing’. MSCS. Mathematical Structures in Computer Science, 14, February 2004. URL: https://doi.org/10.1017/S0960129503004080.
  6. 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.
  7. Simon Castellan, Pierre Clairambault, and Peter Dybjer. Categories with families: Unityped, simply typed, and dependently typed. In Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, pages 135-180. Springer, 2021. Google Scholar
  8. Pierre-Louis Curien. Substitution up to Isomorphism. Fundam. Informaticae, 19(1/2):51-85, 1993. Google Scholar
  9. Pierre-Louis Curien, Richard Garner, and Martin Hofmann. Revisiting the categorical interpretation of dependent type theory. Theor. Comput. Sci., 546:99-119, 2014. URL: https://doi.org/10.1016/j.tcs.2014.03.003.
  10. 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.
  11. Nicola Gambino and Richard Garner. The identity type weak factorisation system. Theor. Comput. Sci., 409(1):94-109, 2008. URL: https://doi.org/10.1016/j.tcs.2008.08.030.
  12. Nicola Gambino and Simon Henry. Towards a constructive simplicial model of Univalent Foundations. Journal of the London Mathematical Society, 105, 2022. Google Scholar
  13. Joseph A. Goguen. What is unification? - a categorical view of substitution, equation and solution. In Resolution of Equations in Algebraic Structures, Volume 1: Algebraic Techniques, pages 217-261. Academic, 1989. Google Scholar
  14. 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.
  15. Martin Hofmann. Syntax and semantics of dependent types, pages 13-54. Springer London, London, 1997. URL: https://doi.org/10.1007/978-1-4471-0963-1_2.
  16. Valery Isaev. Model structures on categories of models of type theories. Mathematical Structures in Computer Science, 28:1695-1722, 2017. Google Scholar
  17. Valery Isaev. Morita equivalences between algebraic dependent type theories. CoRR, abs/1804.05045, 2018. URL: http://arxiv.org/abs/1804.05045.
  18. Valery Isaev. Indexed type theories. Math. Struct. Comput. Sci., 31(1):3-63, 2021. URL: https://doi.org/10.1017/S0960129520000092.
  19. Chris Kapulkin and Peter Lumsdaine. The homotopy theory of type theories. Advances in Mathematics, 337, September 2016. URL: https://doi.org/10.1016/j.aim.2018.08.003.
  20. Krzysztof Kapulkin and Peter Lumsdaine. Homotopical inverse diagrams in categories with attributes. Journal of Pure and Applied Algebra, 225:106563, April 2021. URL: https://doi.org/10.1016/j.jpaa.2020.106563.
  21. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of Univalent Foundations (after Voevodsky). Journal of the European Mathematical Society, 23(6):2071-2126, 2021. Google Scholar
  22. 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.
  23. Paige Randall North. Identity types and weak factorization systems in Cauchy complete categories. Math. Struct. Comput. Sci., 29(9):1411-1427, 2019. URL: https://doi.org/10.1017/S0960129519000033.
  24. J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23-41, January 1965. URL: https://doi.org/10.1145/321250.321253.
  25. Michael Shulman. Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science, 25(5):1203-1277, 2015. URL: https://doi.org/10.1017/S0960129514000565.
  26. Taichi Uemura. A general framework for the semantics of type theory. CoRR, abs/1904.04097, 2019. URL: http://arxiv.org/abs/1904.04097.
  27. Taichi Uemura. Abstract and concrete type theories. PhD thesis, Institute for Logic, Language and Computation, 2021. URL: https://dare.uva.nl/search?identifier=41ff0b60-64d4-4003-8182-c244a9afab3b.
  28. Benno van den Berg. Path categories and propositional identity types. ACM Trans. Comput. Log., 19(2):15:1-15:32, 2018. URL: https://doi.org/10.1145/3204492.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact