Definition from_opp_opp_to_opp (A C : precategory) (hsC : has_homsets C) : functor_data [A^op, C^op, has_homsets_opp hsC] [A, C, hsC]^op. Proof. use tpair; simpl. - intro F. use tpair. + exists F. apply (λ a b f, # F f). + abstract (split; [ intro a; apply (functor_id F) | intros a b c f g; apply (functor_comp F)]). - intros F G α; exists α. abstract (intros a b f; apply pathsinv0, (nat_trans_ax α)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.FunctorCategory.