Type theory in type theory using quotient inductive types

3 years 11 days ago
Type theory in type theory using quotient inductive types
We present an internal formalisation of dependent type theory in type theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids refering to preterms or a typability relation but defines directly well typed objects by an inductive definition. We use the elimination principle to define the set-theoretic and logical predicate interpretation. The work has been formalized using the Agda system extended with QITs using postulates. Categories and Subject Descriptors D.3.1 [Formal Definitions and Theory]; F.4.1 [Mathematical Logic]: Lambda calculus and related systems Keywords Higher Inductive Types, Homotopy Type Theory, Logical Relations, Metaprogramming
Thorsten Altenkirch, Ambrus Kaposi
Added 09 Apr 2016
Updated 09 Apr 2016
Type Journal
Year 2016
Where POPL
Authors Thorsten Altenkirch, Ambrus Kaposi
Comments (0)