(A : AdjunctionUnit F G) : NaturalTransformation (F o G) 1. Proof. refine (Build_NaturalTransformation (F o G) 1 (fun d => (@center _ (A.2 (G d) d 1)).1) _). abstract ( to_unit_counit_nt counit_natural_transformation__of__adjunction_unit_helper ltac:(fun H => try_associativity_quick rewrite <- H) ). Defined.
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.