Definition opfunctorcat_adjdata_functorcatofoppcats : adjunction_data [C ^opp, D ^opp] ([C, D] ^opp). Proof. use make_adjunction_data. - exact (opfunctorcat_from_functorcatofoppcats C D). - exact (opfunctorcat_to_functorcatofoppcats C D). - exact (unit_opfunctorcat_functorcatofoppcats C D). - exact (counit_opfunctorcat_functorcatofoppcats C D). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.whiskering. Section OppositeOfFunctorCatFromFunctorCatOfOpposite. End OppositeOfFunctorCatFromFunctorCatOfOpposite.