Lemma isofhlevel_hsubtype {X : UU} {n : nat} (isof : isofhlevel (S n) X) : ∏ subt : hsubtype X, isofhlevel (S n) subt. Proof. intros subt. apply isofhleveltotal2. - assumption. - intro. apply isofhlevelsnprop. apply propproperty. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.