Definition Equivalence_toAdjointness {X Y} (f:Equivalence X Y) : ∏ x, maponpaths f (Equivalence_toSourceHomotopy f x) = Equivalence_toTargetHomotopy f (f x) := pr2 (pr2 (pr2 (pr2 f))).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.