Definition total_set_category_has_pb_ump {C₁ C₂ : setcategory} {F : C₁ ⟶ C₂} {G₁ : C₁ ⟶ cat_of_setcategory} {G₂ : C₂ ⟶ cat_of_setcategory} (α : G₁ ⟹ F ∙ G₂) (Hα : is_nat_z_iso α) : has_pb_ump (@make_pb_cone bicat_of_strict_cats C₁ (total_setcategory_of_set_functor G₂) C₂ F (pr1_total_category_of_set_functor G₂) (total_setcategory_of_set_functor G₁) (pr1_total_category_of_set_functor G₁) (functor_total_category_of_set_functor F α) (make_invertible_2cell (is_invertible_2cell_bicat_of_strict_cat (functor_total_category_of_set_functor_comm F α) (is_nat_z_iso_functor_total_category_of_set_functor_comm F α)))). Proof. split. - intro x. use make_pb_1cell. + apply (@total_set_category_pb_ump_1_mor _ _ _ _ _ _ Hα _ (pb_cone_pr1 x) (pb_cone_pr2 x) (pr1 (pb_cone_cell x))). apply from_is_invertible_2cell_bicat_of_strict_cat. apply property_from_invertible_2cell. + use make_invertible_2cell. * apply (@total_set_category_pb_ump_1_mor_pr1 _ _ _ _ _ _ Hα _ (pb_cone_pr1 x) (pb_cone_pr2 x) (pr1 (pb_cone_cell x))). * apply is_invertible_2cell_bicat_of_strict_cat. apply total_set_category_pb_ump_1_mor_pr1_is_nat_z_iso. + use make_invertible_2cell. * apply (@total_set_category_pb_ump_1_mor_pr2 _ _ _ _ _ _ Hα _ (pb_cone_pr1 x) (pb_cone_pr2 x) (pr1 (pb_cone_cell x))). * apply is_invertible_2cell_bicat_of_strict_cat. apply total_set_category_pb_ump_1_mor_pr2_is_nat_z_iso. + abstract (use nat_trans_eq ; [ apply homset_property | ] ; intro z ; cbn ; rewrite (functor_id F) ; rewrite !id_left, id_right ; exact (!(nat_trans_eq_pointwise (vcomp_rinv (pb_cone_cell x)) z))). - intros C₀ φ₁ φ₂ δ₁ δ₂ p. assert (∏ (x : pr1 C₀), pr1 (pr1 δ₂ x) = # F (pr1 δ₁ x)) as q. { abstract (intro x ; pose (nat_trans_eq_pointwise p x) as q ; cbn in q ; rewrite !id_left, !id_right in q ; exact q). } use iscontraprop1. + apply total_set_category_pb_ump_2_unique. apply Hα. + simple refine (_ ,, _ ,, _). * exact (total_set_category_pb_ump_2_cell _ Hα δ₁ δ₂ q). * apply total_set_category_pb_ump_2_pr1. * apply total_set_category_pb_ump_2_pr2. 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.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.DisplayedCats.StreetOpFibration. Require Import UniMath.CategoryTheory.GrothendieckConstruction.TotalCategory. Require Import UniMath.CategoryTheory.GrothendieckConstruction.IsosInTotal. Require Import UniMath.CategoryTheory.GrothendieckConstruction.IsOpfibration. Require Import UniMath.CategoryTheory.GrothendieckConstruction.IsPullback. Require Import UniMath.CategoryTheory.GrothendieckConstruction.Projection. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration. Require Import UniMath.Bicategories.Morphisms.Examples.FibrationsInStrictCats. Require Import UniMath.Bicategories.Core.Examples.StrictCats. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor. Require Import UniMath.Bicategories.DisplayedBicats.CleavingOfBicat. Require Import UniMath.Bicategories.DisplayedBicats.CartesianPseudoFunctor. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Codomain. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FunctorsIntoCat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayMapBicatToDispBicat. Require Import UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.CodomainCleaving. Require Import UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.FunctorsIntoCatCleaving. Require Import UniMath.Bicategories.Limits.Products. Import Products.Notations. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.Logic.ComprehensionBicat.