Definition opfunctorcat_from_functorcatofoppcats_data : functor_data ([C^opp,D^opp]) ([C,D]^opp). Proof. use make_functor_data. - intro F. use make_functor. + exists (λ c, (pr1 F) c). exact (λ c1 c2 f, #(pr1 F) f). + abstract (split ; intro ; intros ; cbn ; [ apply (functor_id F) | apply (functor_comp F) ]). - intros F G α. exists (λ c, pr1 α c). intros c1 c2 f. exact (! pr2 α c2 c1 f). 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.