Write a Blog >>
Wed 20 Jan 2016 10:55 - 11:20 at Grand Bay South - Track 2: Types and Foundations Chair(s): Bob Atkey

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.

Poster (poster.pdf)113KiB