Constructions with non-recursive higher inductive types

Nicolai Kraus

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Citations (Scopus)
116 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationLICS '16 - Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
PublisherAssociation for Computing Machinery (ACM)
ISBN (Print)9781450343916
Publication statusPublished - 5 Jul 2016
EventThe 31st Annual ACM/IEEE Symposium on Logic in Computer Science - New York, United States
Duration: 5 Jul 20168 Jul 2016


ConferenceThe 31st Annual ACM/IEEE Symposium on Logic in Computer Science
Country/TerritoryUnited States
CityNew York


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


Dive into the research topics of 'Constructions with non-recursive higher inductive types'. Together they form a unique fingerprint.

Cite this