C D (F : Functor C D) (G : Functor D C) (A : F -| G) : G^op -| F^op := @Build_AdjunctionUnitCounit _ _ (G^op) (F^op) ((counit A)^op) ((unit A)^op) (unit_counit_equation_2 A) (unit_counit_equation_1 A).
Require Import Category.Core Functor.Core. Require Import Functor.Dual NaturalTransformation.Dual. Require Import Adjoint.UnitCounit Adjoint.Core.