(A : AdjunctionUnit G F) : AdjunctionCounit F^op G^op := exist (fun U : NaturalTransformation (F^op o G^op) 1 => forall (c : C^op) (d : D^op) (g : morphism D^op ((F^op)%functor c) d), Contr {f : morphism C^op c ((G^op)%functor d) | U d o F^op _1 f = g }) (A.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Category.Dual Functor.Dual NaturalTransformation.Dual. Require Import Functor.Composition.Core Functor.Identity.