Constructions with non-recursive higher inductive types
Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to define equalities (paths). We say that a HIT H is non-recursive if its constructors do not quantify...
| Main Author: | |
|---|---|
| Format: | Conference or Workshop Item |
| Published: |
2016
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/33025/ |
| _version_ | 1848794542134788096 |
|---|---|
| author | Kraus, Nicolai |
| author_facet | Kraus, Nicolai |
| author_sort | Kraus, Nicolai |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to define equalities (paths). We say that a HIT H is non-recursive if its constructors do not quantify over elements or paths in H. The advantage of non-recursive HITs is that their elimination principles are easier to apply than those of general HITs.
It is an open question which classes of HITs can be encoded as non-recursive HITs. One result of this paper is the construction of the propositional truncation via a sequence of approximations, yielding a representation as a non-recursive HIT. Compared to a related construction by van Doorn, ours has the advantage that the connectedness level increases in each step, yielding simplified elimination principles into n-types. As the elimination principle of our sequence has strictly lower requirements, we can then prove a similar result for van Doorn’s construction. We further derive general elimination principles of higher truncations (say, k-truncations) into n-types, generalizing a previous result by Capriotti et al. which considered the case n=k+1. |
| first_indexed | 2025-11-14T19:17:51Z |
| format | Conference or Workshop Item |
| id | nottingham-33025 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T19:17:51Z |
| publishDate | 2016 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-330252020-05-04T20:05:20Z https://eprints.nottingham.ac.uk/33025/ Constructions with non-recursive higher inductive types Kraus, Nicolai Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to define equalities (paths). We say that a HIT H is non-recursive if its constructors do not quantify over elements or paths in H. The advantage of non-recursive HITs is that their elimination principles are easier to apply than those of general HITs. It is an open question which classes of HITs can be encoded as non-recursive HITs. One result of this paper is the construction of the propositional truncation via a sequence of approximations, yielding a representation as a non-recursive HIT. Compared to a related construction by van Doorn, ours has the advantage that the connectedness level increases in each step, yielding simplified elimination principles into n-types. As the elimination principle of our sequence has strictly lower requirements, we can then prove a similar result for van Doorn’s construction. We further derive general elimination principles of higher truncations (say, k-truncations) into n-types, generalizing a previous result by Capriotti et al. which considered the case n=k+1. 2016 Conference or Workshop Item PeerReviewed Kraus, Nicolai (2016) Constructions with non-recursive higher inductive types. In: Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), July 5–8, 2016, New York City, USA. (In Press) Homotopy type theory |
| spellingShingle | Homotopy type theory Kraus, Nicolai Constructions with non-recursive higher inductive types |
| title | Constructions with non-recursive higher inductive types |
| title_full | Constructions with non-recursive higher inductive types |
| title_fullStr | Constructions with non-recursive higher inductive types |
| title_full_unstemmed | Constructions with non-recursive higher inductive types |
| title_short | Constructions with non-recursive higher inductive types |
| title_sort | constructions with non-recursive higher inductive types |
| topic | Homotopy type theory |
| url | https://eprints.nottingham.ac.uk/33025/ |