Constructions with Non-Recursive Higher Inductive Types

Kraus, Nicolai

Abstract

© 2016 ACM. 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.

Citation

Kraus, N. (2016). Constructions with Non-Recursive Higher Inductive Types. In LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (595-604). https://doi.org/10.1145/2933575.2933586

• Conference Name: LICS '16: 31st Annual ACM/IEEE Symposium on Logic in Computer Science
• Conference Location: New York NY USA
• Start Date: Jul 5, 2016
• End Date: Jul 8, 2016
• Acceptance Date: Apr 4, 2016
• Online Publication Date: Jul 5, 2016
• Publication Date: Jul 5, 2016
• Deposit Date: Apr 28, 2016
• Publicly Available Date: Jul 5, 2016
• Publisher: Association for Computing Machinery (ACM)
• Volume: 2016-July
• Pages: 595-604
• Book Title: LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
• ISBN: 9781450343916
• DOI: https://doi.org/10.1145/2933575.2933586
• Keywords: Homotopy type theory
• Public URL: https://nottingham-repository.worktribe.com/output/980106
• Publisher URL: https://dl.acm.org/citation.cfm?doid=2933575.2933586
• Additional Information: Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without; fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice; and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be; honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to; lists, contact the Owner/Author. Request permissions from [e-mail] or Publications Dept., ACM, Inc., fax; [phone]. Copyright 20yy held by Owner/Author. Publication Rights Licensed to ACM.