Definition adjunction_data_opposite : adjunction_data (opp_cat D) (opp_cat C). Proof. refine (functor_op G ,, functor_op F ,, _ ,, _). - exists (λ d, counit_from_are_adjoints a d). exact (λ d1 d2 f, ! pr2 (counit_from_are_adjoints a) d2 d1 f). - exists (λ d, unit_from_are_adjoints a d). exact (λ d1 d2 f, ! pr2 (unit_from_are_adjoints a) d2 d1 f). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.OppositeCategory.Core.