Hello all,
Many ways of doing HoTT (Coq + Univalence Axiom, Cubical
Type Theory) make sense without including support for
defining Higher Inductive Types. The possibility of defining
small, closed types which are not hsets (like the circle) or
have infinite h-level (like the 2-sphere, conjectured?)
makes constructing HITs from other types seem difficult,
since all the type formers except universes preserve
h-level.
Does anyone know a proof that it is impossible to
construct some HITs from basic type formers (say 0, 1, 2,
Sigma, Pi, W, and a hierarchy of univalent universes U_n),
up to equivalence?
- Jasper Hugunin
--