(A : AdjunctionUnit F G) s d (m : morphism D s d) (eta := A.1) (eps := fun X => (@center _ (A.2 (G X) X 1)).1) : G _1 (eps d o F _1 (G _1 m)) o eta (G s) = G _1 m -> G _1 (m o eps s) o eta (G s) = G _1 m -> eps d o F _1 (G _1 m) = m o eps s. Proof. intros. transitivity (@center _ (A.2 _ _ (G _1 m))).1; [ symmetry | ]; let x := match goal with |- _ = ?x => constr:(x) end in refine ((fun H => ap pr1 (@contr _ (A.2 _ _ (G _1 m)) (x; H))) _); assumption. Qed.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Adjoint.UnitCounit Adjoint.Dual. Require Import Functor.Composition.Core Functor.Identity. Require Import HoTT.Tactics Basics.Trunc Types.Sigma. Require Import Basics.Tactics.