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