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