proposition: Lemma isofhlevel0pathspace (X Y : UU) : iscontr X -> iscontr Y -> iscontr (X = Y).
proof: Proof. intros pX pY. set (H := isofhlevelweqb 0 (eqweqmap ,, univalenceAxiom X Y)). apply H. clear H. apply iscontr_weq; assumption. Defined.
imports: UniMath.Foundations.Propositions UniMath.Foundations.UnivalenceAxiom