Type theory in type theory using quotient inductive types

Altenkirch, Thorsten; Kaposi, Ambrus

Abstract

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 referring 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.

Citation

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

• Conference Name: POPL '16 The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
• Conference Location: St Petersburg, Florida, USA
• Start Date: Jan 20, 2016
• End Date: Jan 23, 2016
• Acceptance Date: Oct 14, 2015
• Online Publication Date: Jan 20, 2016
• Publication Date: Jan 20, 2016
• Deposit Date: Jan 4, 2016
• Publicly Available Date: Jan 20, 2016
• Journal: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
• Publisher: Association for Computing Machinery (ACM)
• Peer Reviewed: Peer Reviewed
• Volume: 2016-Jan
• Pages: 18-29
• Book Title: POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
• ISBN: 9781450335492
• DOI: https://doi.org/10.1145/2837614.2837638
• Keywords: Higher Inductive Types, Homotopy Type Theory, LogicalRelations, Metaprogramming, Agda
• Public URL: https://nottingham-repository.worktribe.com/output/771860
• Publisher URL: https://dl.acm.org/doi/10.1145/2837614.2837638
• Additional Information: Published in: POPL '16 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York : ACM, c2016, p. 18-29. ISBN: 9781450335492 doi:10.1145/2837614.2837638