Canonicity for 2-dimensional type theory
- 25 January 2012
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '12
- p. 337-348
- https://doi.org/10.1145/2103656.2103697
Abstract
Higher-dimensional dependent type theory enriches conventional one-dimensional dependent type theory with additional structure expressing equivalence of elements of a type. This structure may be employed in a variety of ways to capture rather coarse identifications of elements, such as a universe of sets considered modulo isomorphism. Equivalence must be respected by all families of types and terms, as witnessed computationally by a type-generic program. Higher-dimensional type theory has applications to code reuse for dependently typed programming, and to the formalization of mathematics. In this paper, we develop a novel judgemental formulation of a two-dimensional type theory, which enjoys a canonicity property: a closed term of boolean type is definitionally equal to true or false. Canonicity is a necessary condition for a computational interpretation of type theory as a programming language, and does not hold for existing axiomatic presentations of higher-dimensional type theory. The method of proof is a generalization of the NuPRL semantics, interpreting types as syntactic groupoids rather than equivalence relations.Keywords
This publication has 10 references indexed in Scilit:
- 2-Dimensional Directed Type TheoryElectronic Notes in Theoretical Computer Science, 2011
- Two-dimensional models of type theoryMathematical Structures in Computer Science, 2009
- Weak ω-Categories from Intensional Type TheoryLecture Notes in Computer Science, 2009
- Homotopy theoretic models of identity typesMathematical Proceedings of the Cambridge Philosophical Society, 2009
- The identity type weak factorisation systemTheoretical Computer Science, 2008
- Observational equality, now!Published by Association for Computing Machinery (ACM) ,2007
- System F with type equality coercionsPublished by Association for Computing Machinery (ACM) ,2007
- Syntax and Semantics of Dependent TypesPublished by Cambridge University Press (CUP) ,1997
- Constructive mathematics and computer programmingPhilosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences, 1984
- An Intuitionistic Theory of Types: Predicative PartPublished by Elsevier BV ,1975