Definition isEquivalence_toAdjointness {X Y} {f:X->Y} (i:isEquivalence f) : ∏ x, maponpaths f (isEquivalence_toSourceHomotopy i x) = isEquivalence_toTargetHomotopy i (f x) := pr222 i.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.