Library Stdlib.Logic.HLevels

Require Export Stdlib.Logic.HLevelsBase.

From Stdlib.Logic Require Import FunctionalExtensionality.

Lemma forall_hprop : forall (A : Type) (P : A -> Prop),
    (forall x:A, IsHProp (P x))
    -> IsHProp (forall x:A, P x).

Lemma impl_hprop : forall P Q : Prop,
    IsHProp Q -> IsHProp (P -> Q).

Lemma not_hprop : forall P : Type, IsHProp (P -> False).

Lemma hprop_hprop : forall X : Type,
    IsHProp (IsHProp X).

Lemma hprop_hset : forall X : Type,
    IsHProp (IsHSet X).