proposition: Lemma isofhlevelSnpathspace : ∏ n : nat, ∏ X Y : UU, isofhlevel (S n) Y -> isofhlevel (S n) (X = Y).
proof: Proof. intros n X Y pY. set (H:=isofhlevelweqb (S n) (eqweqmap ,, univalenceAxiom X Y)). apply H. apply isofhlevelsnweqtohlevelsn. assumption. Defined.
imports: UniMath.Foundations.Propositions UniMath.Foundations.UnivalenceAxiom