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