Lemma isofhlevelpathspace : ∏ n : nat, ∏ X Y : UU, isofhlevel n X -> isofhlevel n Y -> isofhlevel n (X = Y). Proof. intros n. induction n as [| n _ ]. - intros X Y pX pY. apply isofhlevel0pathspace; assumption. - intros. apply isofhlevelSnpathspace; assumption. Defined.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.UnivalenceAxiom.