(A : AdjunctionUnit F G) (Y : C) (eta := A.1) (eps := fun X => (@center _ (A.2 (G X) X 1)).1) : G _1 (eps (F Y) o F _1 (eta Y)) o eta Y = eta Y -> eps (F Y) o F _1 (eta Y) = 1. Proof. intros. etransitivity; [ symmetry | ]; simpl_do_clear ltac:(fun H => apply H) (fun y H => (@contr _ (A.2 _ _ (A.1 Y)) (y; H))..1); try assumption. simpl. rewrite ?identity_of, ?left_identity, ?right_identity; reflexivity. 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.