Definition indexed_cat_to_psfunctor {C : category} (Φ : indexed_cat C) : psfunctor (cat_to_bicat C) bicat_of_univ_cats. Proof. use make_psfunctor_from_cat. - exact Φ. - exact (λ _ _ f, Φ $ f). - intro x. use nat_z_iso_to_invertible_2cell. use make_nat_z_iso. + exact (indexed_cat_id Φ x). + intro xx. exact (is_z_isomorphism_indexed_cat_id Φ xx). - intros x y z f g. use nat_z_iso_to_invertible_2cell. use make_nat_z_iso. + exact (indexed_cat_comp Φ f g). + intro xx. exact (is_z_isomorphism_indexed_cat_comp Φ f g xx). - abstract (intros x y f ; use nat_trans_eq ; [ apply homset_property | ] ; cbn ; intro xx ; refine (indexed_cat_lunitor Φ f xx @ _) ; apply maponpaths ; refine (!_) ; refine (idtoiso_2_1_in_bicat_of_univ_cats (maponpaths (λ h, Φ $ h) (id_left f)) xx @ _) ; do 2 apply maponpaths ; exact (maponpathscomp (λ h, Φ $ h) (λ H, pr11 H xx) (id_left f))). - abstract (intros x y f ; use nat_trans_eq ; [ apply homset_property | ] ; cbn ; intro xx ; refine (indexed_cat_runitor Φ f xx @ _) ; apply maponpaths ; refine (!_) ; refine (idtoiso_2_1_in_bicat_of_univ_cats (maponpaths (λ h, Φ $ h) (id_right f)) xx @ _) ; do 2 apply maponpaths ; exact (maponpathscomp (λ h, Φ $ h) (λ H, pr11 H xx) (id_right f))). - abstract (intros w x y z f g h ; use nat_trans_eq ; [ apply homset_property | ] ; cbn ; intro ww ; rewrite id_left ; refine (_ @ indexed_cat_lassociator Φ f g h ww) ; apply maponpaths ; refine (idtoiso_2_1_in_bicat_of_univ_cats (maponpaths (λ h, Φ $ h) (assoc f g h)) ww @ _) ; do 2 apply maponpaths ; exact (maponpathscomp (λ h, Φ $ h) (λ H, pr11 H ww) (assoc f g h))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategory. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Discreteness. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Examples.DiscreteBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Section PseudoFunctorFromCat. End PseudoFunctorFromCat.