Definition functors_into_cat_comprehension_data : disp_psfunctor_data disp_bicat_of_functors_into_cat (cod_disp_bicat bicat_of_strict_cats) (id_psfunctor bicat_of_strict_cats). Proof. simple refine (_ ,, _ ,, _ ,, _ ,, _). - exact (λ C F, total_setcategory_of_set_functor F ,, pr1_total_category_of_set_functor F). - refine (λ C₁ C₂ F G₁ G₂ α, functor_total_category_of_set_functor F α ,, _). use make_invertible_2cell. + exact (functor_total_category_of_set_functor_comm F α). + apply is_invertible_2cell_bicat_of_strict_cat. exact (is_nat_z_iso_functor_total_category_of_set_functor_comm F α). - refine (λ C₁ C₂ F₁ F₂ α G₁ G₂ β₁ β₂ p, nat_trans_total_category_of_set_functor α β₁ β₂ p ,, _). abstract (use nat_trans_eq ; [ apply C₂ | ] ; intro x ; cbn ; rewrite id_left, id_right ; apply idpath). - intros C F. simple refine (_ ,, _). + simple refine (_ ,, _). * exact (functor_total_category_of_set_functor_on_id F). * abstract (use nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; rewrite !id_left ; apply idpath). + use is_disp_invertible_2cell_cod. use is_invertible_2cell_bicat_of_strict_cat. exact (is_nat_z_iso_functor_total_category_of_set_functor_on_id F). - intros C₁ C₂ C₃ F₁ F₂ G₁ G₂ G₃ α β. simple refine (_ ,, _). + simple refine (_ ,, _). * exact (functor_total_category_of_set_functor_on_comp α β). * abstract (use nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; rewrite !id_left ; rewrite (functor_id F₂) ; rewrite !id_right ; apply idpath). + use is_disp_invertible_2cell_cod. use is_invertible_2cell_bicat_of_strict_cat. exact (is_nat_z_iso_functor_total_category_of_set_functor_on_comp α β). 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.