C D (F : Functor C D) (G : Functor D C) (A : F -| G) : (A^op)^op = A := idpath.
Require Import Category.Core Functor.Core. Require Import Functor.Dual NaturalTransformation.Dual. Require Import Adjoint.UnitCounit Adjoint.Core.