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
--