proposition: Theorem isofhlevelfsnfib (n : nat) {X : UU} (P : X -> UU) (x : X) (is : isofhlevel (S n) (x = x)) : isofhlevelf (S n) (tpair P x).
proof: Proof. intros. unfold isofhlevelf. intro xp. apply (isofhlevelweqf (S n) (ezweq1pr1 P x xp)). apply isofhlevelsn. intro X1. induction X1. assumption. Defined.
imports: UniMath.Foundations.PartA