Definition disp_map_bicat_comprehension_data : disp_psfunctor_data DD (cod_disp_bicat B) (id_psfunctor B). Proof. simple refine (_ ,, _ ,, _ ,, _ ,, _). - exact (λ x hx, pr1 hx ,, pr12 hx). - exact (λ x y f hx hy hf, pr1 hf ,, pr22 hf). - exact (λ x y f g α hx hy hf hg hα, hα). - simple refine (λ x hx, _ ,, _). + use make_disp_2cell_cod. * exact (id₂ _). * abstract (unfold coherent_homot ; cbn ; rewrite id2_rwhisker, id2_right ; rewrite lwhisker_id2, id2_left ; apply idpath). + use is_disp_invertible_2cell_cod ; simpl. is_iso. - simple refine (λ x y z f g hx hy hz hf hg, _ ,, _). + use make_disp_2cell_cod. * exact (id₂ _). * abstract (unfold coherent_homot ; cbn ; rewrite id2_rwhisker, id2_right ; rewrite lwhisker_id2, id2_left ; rewrite !vassocl ; apply idpath). + use is_disp_invertible_2cell_cod ; simpl. is_iso. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration. Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration. Require Import UniMath.Bicategories.Logic.DisplayMapBicat. 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.DisplayMapBicatToDispBicat. Require Import UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.CodomainCleaving. Require Import UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.DisplayMapBicatCleaving. Require Import UniMath.Bicategories.Limits.Pullbacks. 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.