## Abstract

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.

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.

Original language | English |
---|---|

Title of host publication | LICS '16 - Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science |

Publisher | Association for Computing Machinery (ACM) |

Pages | 595-604 |

ISBN (Print) | 9781450343916 |

DOIs | |

Publication status | Published - 5 Jul 2016 |

Event | The 31st Annual ACM/IEEE Symposium on Logic in Computer Science - New York, United States Duration: 5 Jul 2016 → 8 Jul 2016 |

### Conference

Conference | The 31st Annual ACM/IEEE Symposium on Logic in Computer Science |
---|---|

Country/Territory | United States |

City | New York |

Period | 5/07/16 → 8/07/16 |

## Keywords

- homotopy type theory
- higher inductive types
- sequential colimits
- truncation elimination
- van Doorn construction