The first three levels of homotopy type theory: homotopy propositions,
homotopy sets and homotopy one types. For more information,
https://github.com/HoTT/HoTT
and
https://homotopytypetheory.org/book
Univalence is not assumed here, and equality is Coq's usual inductive
type eq in sort Prop. This is a little different from HoTT, where
sort Prop does not exist and equality is directly in sort Type.