Type theory in type theory using quotient inductive types
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...
| Main Authors: | , |
|---|---|
| Format: | Conference or Workshop Item |
| Published: |
ACM
2016
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/31169/ |
| _version_ | 1848794141025107968 |
|---|---|
| author | Altenkirch, Thorsten Kaposi, Ambrus |
| author_facet | Altenkirch, Thorsten Kaposi, Ambrus |
| author_sort | Altenkirch, Thorsten |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T19:11:28Z |
| format | Conference or Workshop Item |
| id | nottingham-31169 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T19:11:28Z |
| publishDate | 2016 |
| publisher | ACM |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-311692020-05-04T17:30:29Z https://eprints.nottingham.ac.uk/31169/ Type theory in type theory using quotient inductive types Altenkirch, Thorsten Kaposi, Ambrus 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. ACM 2016-01-22 Conference or Workshop Item PeerReviewed Altenkirch, Thorsten and Kaposi, Ambrus (2016) Type theory in type theory using quotient inductive types. In: POPL '16 The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 20-22 January 2016, St Petersburg, Florida, United States of America. Higher Inductive Types Homotopy Type Theory Logical Relations Metaprogramming Agda http://dl.acm.org/citation.cfm?doid=2837614.2837638 |
| spellingShingle | Higher Inductive Types Homotopy Type Theory Logical Relations Metaprogramming Agda Altenkirch, Thorsten Kaposi, Ambrus Type theory in type theory using quotient inductive types |
| title | Type theory in type theory using quotient inductive types |
| title_full | Type theory in type theory using quotient inductive types |
| title_fullStr | Type theory in type theory using quotient inductive types |
| title_full_unstemmed | Type theory in type theory using quotient inductive types |
| title_short | Type theory in type theory using quotient inductive types |
| title_sort | type theory in type theory using quotient inductive types |
| topic | Higher Inductive Types Homotopy Type Theory Logical Relations Metaprogramming Agda |
| url | https://eprints.nottingham.ac.uk/31169/ https://eprints.nottingham.ac.uk/31169/ |