Definition Equivalence_to_weq {X Y} : X ≅ Y -> X ≃ Y. Proof. intros w. exact (make_weq (Equivalence_toFunction w) (isEquivalence_to_isweq (Equivalence_to_isEquivalence w))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.