Skip to main content

Research Repository

Advanced Search

All Outputs (2)

Type theory in type theory using quotient inductive types (2016)
Presentation / Conference Contribution
Altenkirch, T., & Kaposi, A. (2016). Type theory in type theory using quotient inductive types. In POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (18-29). https://doi.org/10.1145/2837614.2837638

We present an internal formalisation of a type heory with dependent types 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 r... Read More about Type theory in type theory using quotient inductive types.