Loïc Pujet
Abstract
Building on the recent extension of dependent type theory with a universe of definitionally proof-irrelevant types, we introduce TTobs, a new type theory based on the setoidal interpretation of dependent type theory. TTobs equips every type with an identity relation that satisfies function extensionality, propositional extensionality, and definitional uniqueness of identity proofs (UIP). Compared to other existing proposals to enrich dependent type theory with these principles, our theory features a notion of reduction that is normalizing and provides an algorithmic canonicity result, which we formally prove in Agda using the logical relation framework of Abel et al. Our paper thoroughly develops the meta-theoretical properties of TTobs, such as the decidability of the conversion and of the type checking, as well as consistency. We also explain how to extend our theory with quotient types, and we introduce a setoidal version of Swan's Id types that turn it into a proper extension of MLTT with inductive equality.
Supplemental Material
- Andreas Abel and Thierry Coquand. 2020. Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. Logical Methods in Computer Science, Volume 16, Issue 2 (2020), June, https://doi.org/10.23638/LMCS-16(2:14)2020 Google Scholar
Cross Ref
- Andreas Abel, Joakim Öhman, and Andrea Vezzosi. 2018. Decidability of Conversion for Type Theory in Type Theory. Proceedings of the ACM on Programming Languages, 2, POPL (2018), Article 23, Jan., 29 pages. issn:2475-1421 https://doi.org/10.1145/3158111 Google ScholarDigital Library
- Peter Aczel. 1978. The Type Theoretic Interpretation of Constructive Set Theory. In Logic Colloquium ’77, Angus Macintyre, Leszek Pacholski, and Jeff Paris (Eds.) (Studies in Logic and the Foundations of Mathematics, Vol. 96). Elsevier, 55–66. issn:0049-237X https://doi.org/10.1016/S0049-237X(08)71989-X Google ScholarCross Ref
- T. Altenkirch. 1999. Extensional equality in intensional type theory. In Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158). 412–420. issn:1043-6871 https://doi.org/10.1109/LICS.1999.782636 Google ScholarCross Ref
- Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, and Nicolas Tabareau. 2019. Setoid type theory - a syntactic translation. In MPC 2019 - 13th International Conference on Mathematics of Program Construction (LNCS, Vol. 11825). Springer, 155–196. https://doi.org/10.1007/978-3-030-33636-3_7 Google ScholarDigital Library
- Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. 2016. Extending Homotopy Type Theory with Strict Equality. In CSL. https://doi.org/10.4230/LIPIcs.CSL.2016.21 Google ScholarCross Ref
- Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. 2007. Observational equality, now!. In Proceedings of the Workshop on Programming Languages meets Program Verification (PLPV 2007). 57–68. https://doi.org/10.1145/1292597.1292608 Google ScholarDigital Library
- Paolo Capriotti. 2017. Models of type theory with strict equality. Ph.D. Dissertation. University of Nottingham.Google Scholar
- Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter. 2021. The Taming of the Rew: A Type Theory with Computational Assumptions. Proc. ACM Program. Lang., 5, POPL (2021), Article 60, Jan., 29 pages. https://doi.org/10.1145/3434341 Google ScholarDigital Library
- Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2015. Cubical Type Theory: a constructive interpretation of the univalence axiom. In 21st International Conference on Types for Proofs and Programs (21st International Conference on Types for Proofs and Programs). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Tallinn, Estonia. 262. https://doi.org/10.4230/LIPIcs.TYPES.2015.5 Google ScholarCross Ref
- Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. On Higher Inductive Types in Cubical Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’18). Association for Computing Machinery, New York, NY, USA. 255–264. isbn:9781450355834 https://doi.org/10.1145/3209108.3209197 Google ScholarDigital Library
- Peter Dybjer. 1996. Internal type theory. In Types for Proofs and Programs, Stefano Berardi and Mario Coppo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 120–134. isbn:978-3-540-70722-6 https://doi.org/10.1007/3-540-61780-9_66 Google ScholarCross Ref
- Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. 2019. Definitional Proof-Irrelevance without K. Proceedings of the ACM on Programming Languages, 3 (2019), Jan., 1–28. https://doi.org/10.1145/3290316 Google ScholarDigital Library
- Jean-Yves Girard. 1972. Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérieur. Thèse de Doctorat d’État, Université de Paris VII.Google Scholar
- Martin Hofmann. 1993. Non Strictly Positive Datatypes in System F. Email on the Types mailing list. http://www.seas.upenn.edu/~sweirich/types/archive/1993/msg00027.htmlGoogle Scholar
- Martin Hofmann. 1995. Extensional concepts in intensional type theory. Ph.D. Dissertation. University of Edinburgh.Google Scholar
- Chris Kapulkin and Peter LeFanu Lumsdaine. 2018. The simplicial model of Univalent Foundations (after Voevodsky). arxiv:1211.2851.Google Scholar
- Meven Lennon-Bertrand. 2021. Complete Bidirectional Typing for the Calculus of Inductive Constructions. In 12th International Conference on Interactive Theorem Proving (ITP 2021), Liron Cohen and Cezary Kaliszyk (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 193). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. isbn:978-3-95977-188-7 issn:1868-8969 https://doi.org/10.4230/LIPIcs.ITP.2021.24 Google ScholarCross Ref
- Per Martin-Löf. 1975. An Intuitionistic Theory of Types: Predicative Part. In Logic Colloquium ’73, H.E. Rose and J.C. Shepherdson (Eds.) (Studies in Logic and the Foundations of Mathematics, Vol. 80). Elsevier, 73 – 118. issn:0049-237X https://doi.org/10.1016/S0049-237X(08)71945-1 Google ScholarCross Ref
- Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. 2019. Cubical Syntax for Reflection-Free Extensional Equality. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Herman Geuvers (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 131). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 31:1–31:25. isbn:978-3-95977-107-8 issn:1868-8969 https://doi.org/10.4230/LIPIcs.FSCD.2019.31 Google ScholarCross Ref
- Andrew Swan. 2016. An algebraic weak factorisation system on 01-substitution sets: a constructive proof. Journal of Logic and Analysis, issn:1759-9008 https://doi.org/10.4115/jla.2016.8.1 Google ScholarCross Ref
- The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. https://homotopytypetheory.org/book/Google Scholar
- Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. 2019. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. Proc. ACM Program. Lang., 3, ICFP (2019), Article 87, July, 29 pages. https://doi.org/10.1145/3341691 Google ScholarDigital Library
- Vladimir Voevodsky. 2013. A simple type system with two identity types. https://ncatlab.org/homotopytypetheory/files/HTS.pdfGoogle Scholar
- Vladimir Voevodsky. 2015. A C-system defined by a universe category. Theory Appl. Categ., 30 (2015), No. 37, 1181– 1215. issn:1201-561X http://www.tac.mta.ca/tac/volumes/30/37/30-37abs.htmlGoogle Scholar
Index Terms
- Observational equality: now for good
Recommendations
Impredicative Observational Equality
In dependent type theory, impredicativity is a powerful logical principle that allows the definition of propositions that quantify over arbitrarily large types, potentially resulting in self-referential propositions. Impredicativity can provide a system ...
The taming of the rew: a type theory with computational assumptions
Dependently typed programming languages and proof assistants such as Agda and Coq rely on computation to automatically simplify expressions during type checking. To overcome the lack of certain programming primitives or logical principles in those ...
Observational equality, now!
PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verificationThis paper has something new and positive to say about propositional equality in programming and proof systems based on the Curry-Howard correspondence between propositions and types. We have found a way to present a propositional equality type
- which is ...
Comments