Definition trivial_comprehension_data : disp_psfunctor_data (trivial_displayed_bicat B B) (cod_disp_bicat B) (id_psfunctor B). Proof. simple refine (_ ,, _ ,, _ ,, _ ,, _). - intros x y. use make_ar. + exact (x ⊗ y). + exact π₁. - intros x₁ x₂ f y₁ y₂ g. use make_disp_1cell_cod. + exact (f ⊗₁ g). + apply inv_of_invertible_2cell. apply pair_1cell_pr1. - intros x₁ x₂ f₁ f₂ α y₁ y₂ g₁ g₂ β. use make_disp_2cell_cod. + exact (α ⊗₂ β). + abstract (unfold coherent_homot ; cbn ; use vcomp_move_R_pM ; [ is_iso | ] ; cbn ; rewrite !vassocr ; use vcomp_move_L_Mp ; [ is_iso | ] ; cbn ; apply prod_2cell_pr1_alt). - intro ; intros ; simpl. simple refine (_ ,, _). + use make_disp_2cell_cod. * exact ((pair_1cell_id_id_invertible _ _ _)^-1). * abstract (unfold coherent_homot ; cbn ; refine (maponpaths _ (binprod_ump_2cell_pr1 _ _ _) @ _) ; rewrite !vassocr ; apply maponpaths_2 ; rewrite lwhisker_id2 ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite linvunitor_lunitor ; rewrite id2_left ; apply runitor_rinvunitor). + use is_disp_invertible_2cell_cod. cbn. apply binprod_ump_2cell_invertible ; is_iso. - intro ; intros ; simpl. simple refine (_ ,, _). + use make_disp_2cell_cod. * apply pair_1cell_comp. * abstract (unfold coherent_homot ; cbn ; rewrite !vassocl ; etrans ; [ do 5 apply maponpaths ; apply binprod_ump_2cell_pr1 | ] ; rewrite !vassocr ; apply maponpaths_2 ; rewrite !vassocl ; etrans ; [ do 4 apply maponpaths ; rewrite !vassocr ; rewrite lassociator_rassociator ; rewrite id2_left ; apply idpath | ] ; etrans ; [ do 3 apply maponpaths ; rewrite !vassocr ; rewrite lwhisker_vcomp ; rewrite vcomp_linv ; rewrite lwhisker_id2 ; rewrite id2_left ; apply idpath | ] ; etrans ; [ do 2 apply maponpaths ; rewrite !vassocr ; rewrite rassociator_lassociator ; rewrite id2_left ; apply idpath | ] ; etrans ; [ apply maponpaths ; rewrite !vassocr ; rewrite rwhisker_vcomp ; rewrite vcomp_linv ; rewrite id2_rwhisker ; rewrite id2_left ; apply idpath | ] ; rewrite lassociator_rassociator ; rewrite lwhisker_id2 ; apply idpath). + use is_disp_invertible_2cell_cod. cbn. apply pair_1cell_comp_invertible. 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.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.Properties. Require Import UniMath.Bicategories.Morphisms.Properties.Projections. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.CleavingOfBicat. Require Import UniMath.Bicategories.DisplayedBicats.CartesianPseudoFunctor. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Trivial. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Codomain. Require Import UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.TrivialCleaving. Require Import UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.CodomainCleaving. 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.