Library Stdlib.Logic.HLevelsBase
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.
Definition IsHProp (P : Type) : Prop
:= forall p q : P, p = q.
Definition IsHSet (X : Type) : Prop
:= forall (x y : X) (p q : x = y), p = q.
Definition IsHOneType (X : Type) : Prop
:= forall (x y : X) (p q : x = y) (r s : p = q), r = s.
Lemma and_hprop : forall P Q : Prop,
IsHProp P -> IsHProp Q -> IsHProp (P /\ Q).
Lemma hset_hprop : forall X : Type,
IsHProp X -> IsHSet X.
Lemma eq_trans_cancel : forall {X : Type} {x y z : X} (p : x = y) (q r : y = z),
(eq_trans p q = eq_trans p r) -> q = r.
Lemma hset_hOneType : forall X : Type,
IsHSet X -> IsHOneType X.
Definition false_hprop : IsHProp False :=
fun p => match p with end.
Definition true_hprop : IsHProp True :=
fun p q => match p, q with I, I => eq_refl end.