proposition: Theorem isofhlevelsnsummand1 (n : nat) (X Y : UU) : isofhlevel (S n) (coprod X Y) -> isofhlevel (S n) X.
proof: Proof. intros is. apply (isofhlevelXfromfY (S n) (@ii1 X Y) (isofhlevelfsnincl n _ (isinclii1 _ _)) is). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom