Definition functorcategoryright_psfunctor: psfunctor CAT CAT. Proof. use make_psfunctor. - exact functorcategoryright_map_data. - exact functorcategoryright_map_laws. - split; red; cbn. + intro B. use tpair. * use make_nat_trans. -- intro G. cbn. apply ρ_functors. -- intros G G' α. apply (nat_trans_eq (homset_property _)). intro a. cbn. rewrite id_left; apply id_right. * split; apply (nat_trans_eq (homset_property (functor_category _ _))); intro G; cbn; apply (nat_trans_eq (homset_property _)); intro a; apply id_left. + intros B1 B2 B3 F H. use tpair. * use make_nat_trans. -- intro G. cbn. apply α_functors_inv. -- intros G G' α. apply (nat_trans_eq (homset_property _)). intro a. cbn. rewrite id_left; apply id_right. * split; apply (nat_trans_eq (homset_property (functor_category _ _))); intro G; cbn; apply (nat_trans_eq (homset_property _)); intro a; apply id_left. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Biadjunction. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.Modifications.Modification. Import Bicat.Notations.