Definition opcleaving_comprehension_data : disp_psfunctor_data disp_bicat_of_opcleaving (cod_disp_bicat bicat_of_univ_cats) (id_psfunctor bicat_of_univ_cats). Proof. simple refine (_ ,, _ ,, _ ,, _ ,, _). - exact (λ C D, total_univalent_category (pr1 D) ,, pr1_category _). - intros C₁ C₂ F D₁ D₂ FF. use make_disp_1cell_cod. + exact (total_functor (pr1 FF)). + use nat_z_iso_to_invertible_2cell. exact (total_functor_commute_z_iso (pr1 FF)). - intros C₁ C₂ F G α D₁ D₂ FF GG αα. use make_disp_2cell_cod. + exact (total_nat_trans (pr1 αα)). + abstract (use nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; rewrite id_left, id_right ; apply idpath). - intros C D. simple refine (_ ,, _). + use make_disp_2cell_cod. * exact (total_functor_identity (pr11 D)). * abstract (use nat_trans_eq ; [ apply homset_property | ] ; intros x ; cbn ; rewrite !id_left ; apply idpath). + use is_disp_invertible_2cell_cod. use is_nat_z_iso_to_is_invertible_2cell. intro x. apply identity_is_z_iso. - intros C₁ C₂ C₃ F G D₁ D₂ D₃ FF GG. simple refine (_ ,, _). + use make_disp_2cell_cod. * exact (total_functor_comp (pr1 FF) (pr1 GG)). * abstract (use nat_trans_eq ; [ apply homset_property | ] ; intros x ; cbn ; rewrite !id_left, !id_right ; apply functor_id). + use is_disp_invertible_2cell_cod. use is_nat_z_iso_to_is_invertible_2cell. intro x. apply identity_is_z_iso. 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.whiskering. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.StreetFibration. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. 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.DispBicatOfDispCats. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Codomain. Require Import UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.CodomainCleaving. Require Import UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.OpFibrationCleaving. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.Examples.BicatOfUnivCatsLimits. Require Import UniMath.Bicategories.Limits.Examples.OpCellBicatLimits. 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.