Library Coq.Logic.HLevels
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.
Require Import Coq.Logic.FunctionalExtensionality.
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 forall_hprop : forall (A : Type) (P : A -> Prop),
(forall x:A, IsHProp (P x))
-> IsHProp (forall x:A, P x).
Lemma and_hprop : forall P Q : Prop,
IsHProp P -> IsHProp Q -> IsHProp (P /\ Q).
Lemma impl_hprop : forall P Q : Prop,
IsHProp Q -> IsHProp (P -> Q).
Lemma false_hprop : IsHProp False.
Lemma true_hprop : IsHProp True.
Lemma not_hprop : forall P : Type, IsHProp (P -> False).
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.
Lemma hprop_hprop : forall X : Type,
IsHProp (IsHProp X).
Lemma hprop_hset : forall X : Type,
IsHProp (IsHSet X).