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