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

• Type: Journal
• Year: 2016
• Where: POPL
• Authors: Thorsten Altenkirch, Ambrus Kaposi
• Keywords: POPL 2016, Programming Languages