fact: Definition adjunction_unit__op__adjunction_counit (A : AdjunctionCounit G^op F^op) : AdjunctionUnit F G := exist (fun T : NaturalTransformation 1 (G o F) => forall (c : C) (d : D) (f : morphism C c (G d)), Contr { g : morphism D (F c) d | G _1 g o T c = f }) (A.1^op)%natural_transformation (fun c d g => A.2 d c g).
imports: Category.Core Functor.Core NaturalTransformation.Core Category.Dual Functor.Dual NaturalTransformation.Dual Functor.Composition.Core Functor.Identity