Lemma is_functor_from_opp_opp_to_opp (A C : precategory) (hsC : has_homsets C) : is_functor (from_opp_opp_to_opp A C hsC). Proof. split. - now intro F; simpl; apply (nat_trans_eq hsC); intro a. - now intros F G H α β; simpl; apply (nat_trans_eq hsC); intro a. Qed.
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.