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