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