proposition: Lemma check3 X Y (w:X≅Y) : Equivalence_toTargetHomotopy (weq_to_Equivalence (Equivalence_to_weq w)) = Equivalence_toTargetHomotopy w.
proof: Proof. reflexivity. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Tactics