Definition disp_map_bicat_to_disp_prebicat_ops : disp_prebicat_ops disp_map_bicat_to_disp_prebicat_1_id_comp_cells. Proof. repeat split. - intros x y f hx hy hf ; cbn in *. use make_disp_map_bicat_cell. + exact (id2 _). + abstract (rewrite id2_rwhisker, lwhisker_id2 ; rewrite id2_left, id2_right ; apply idpath). - intros x y f hx hy hf ; cbn in *. use make_disp_map_bicat_cell. + exact (lunitor _). + abstract (cbn ; rewrite <- rwhisker_vcomp ; rewrite !vassocr ; rewrite runitor_rwhisker ; rewrite !vassocl ; apply maponpaths ; rewrite lunitor_triangle ; rewrite vcomp_lunitor ; rewrite !vassocr ; rewrite <- linvunitor_assoc ; rewrite linvunitor_lunitor ; apply id2_left). - intros x y f hx hy hf ; cbn in *. use make_disp_map_bicat_cell. + exact (runitor _). + abstract (cbn ; rewrite <- !lwhisker_vcomp ; rewrite !vassocl ; rewrite runitor_rwhisker ; rewrite lwhisker_vcomp ; rewrite linvunitor_lunitor ; rewrite lwhisker_id2 ; rewrite id2_right ; rewrite runitor_triangle ; rewrite vcomp_runitor ; rewrite !vassocr ; apply maponpaths_2 ; exact (!(left_unit_assoc _ _))). - intros x y f hx hy hf ; cbn in *. use make_disp_map_bicat_cell. + exact (linvunitor _). + abstract (cbn ; rewrite <- !rwhisker_vcomp ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite runitor_rwhisker ; rewrite !vassocr ; rewrite lwhisker_vcomp ; rewrite linvunitor_lunitor ; rewrite lwhisker_id2 ; rewrite id2_left ; rewrite <- linvunitor_assoc ; rewrite lwhisker_hcomp ; rewrite <- linvunitor_natural ; rewrite !vassocl ; apply maponpaths ; rewrite linvunitor_assoc ; rewrite !vassocl ; rewrite rassociator_lassociator ; rewrite id2_right ; apply idpath). - intros x y f hx hy hf ; cbn in *. use make_disp_map_bicat_cell. + exact (rinvunitor _). + abstract (cbn ; rewrite <- !lwhisker_vcomp ; rewrite !vassocl ; rewrite !lwhisker_hcomp ; rewrite triangle_l_inv ; rewrite <- !lwhisker_hcomp, <- rwhisker_hcomp ; rewrite !vassocr ; apply maponpaths_2 ; rewrite !vassocl ; rewrite runitor_triangle ; rewrite vcomp_runitor ; refine (!(id2_left _) @ _) ; rewrite !vassocr ; apply maponpaths_2 ; rewrite !vassocl ; rewrite <- left_unit_assoc ; rewrite lwhisker_vcomp ; rewrite rinvunitor_runitor ; rewrite lwhisker_id2 ; apply idpath). - intros x₁ x₂ x₃ x₄ f g k hx₁ hx₂ hx₃ hx₄ hf hg hk ; cbn in *. use make_disp_map_bicat_cell. + exact (rassociator _ _ _). + abstract (cbn ; rewrite <- !lwhisker_vcomp, <- !rwhisker_vcomp ; rewrite !vassocl ; use vcomp_move_L_pM ; [ is_iso | ] ; cbn ; rewrite !vassocr ; rewrite lassociator_lassociator ; rewrite !vassocl ; apply maponpaths ; rewrite !vassocr ; rewrite rwhisker_rwhisker ; rewrite !vassocl ; apply maponpaths ; use vcomp_move_L_pM ; [ is_iso | ] ; cbn ; rewrite !vassocr ; rewrite <- lassociator_lassociator ; rewrite !vassocl ; apply maponpaths ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite rwhisker_vcomp ; rewrite lassociator_rassociator ; rewrite id2_rwhisker ; rewrite id2_left ; rewrite !vassocr ; rewrite <- rwhisker_lwhisker ; rewrite !vassocl ; apply maponpaths ; use vcomp_move_L_pM ; [ is_iso | ] ; cbn ; rewrite !vassocr ; rewrite lassociator_lassociator ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite lassociator_rassociator ; rewrite id2_left ; rewrite !vassocr ; rewrite <- lwhisker_lwhisker ; rewrite !vassocl ; apply maponpaths ; rewrite !vassocr ; rewrite <- lassociator_lassociator ; rewrite !vassocl ; apply maponpaths ; rewrite rwhisker_vcomp ; rewrite lassociator_rassociator ; rewrite id2_rwhisker ; apply id2_right). - intros x₁ x₂ x₃ x₄ f g k hx₁ hx₂ hx₃ hx₄ hf hg hk ; cbn in *. use make_disp_map_bicat_cell. + exact (lassociator _ _ _). + abstract (cbn ; rewrite <- !rwhisker_vcomp, <- !lwhisker_vcomp ; rewrite !vassocr ; rewrite lassociator_lassociator ; rewrite !vassocl ; apply maponpaths ; rewrite !vassocr ; rewrite rwhisker_rwhisker ; rewrite !vassocl ; apply maponpaths ; use vcomp_move_R_pM ; [ is_iso | ] ; cbn ; rewrite !vassocr ; rewrite <- lassociator_lassociator ; rewrite !vassocl ; apply maponpaths ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite rwhisker_vcomp ; rewrite lassociator_rassociator ; rewrite id2_rwhisker ; rewrite id2_left ; rewrite !vassocr ; rewrite <- rwhisker_lwhisker ; rewrite !vassocl ; apply maponpaths ; use vcomp_move_R_pM ; [ is_iso | ] ; cbn ; rewrite !vassocr ; rewrite lassociator_lassociator ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite lassociator_rassociator ; rewrite id2_left ; rewrite !vassocr ; rewrite <- lwhisker_lwhisker ; rewrite !vassocl ; apply maponpaths ; rewrite <- lassociator_lassociator ; rewrite !vassocl ; apply idpath). - intros x₁ x₂ f g h α β hx₁ hx₂ hf hg hh hα hβ ; cbn in *. use make_disp_map_bicat_cell. + exact (pr1 hα • pr1 hβ). + abstract (cbn ; rewrite <- !rwhisker_vcomp ; rewrite <- !lwhisker_vcomp ; rewrite !vassocr ; rewrite (pr2 hα) ; rewrite !vassocl ; rewrite (pr2 hβ) ; apply idpath). - intros x₁ x₂ x₃ f₁ f₂ g α hx₁ hx₂ hx₃ hf₁ hf₂ hg hα ; cbn in *. use make_disp_map_bicat_cell. + exact (_ ◃ pr1 hα). + abstract (cbn ; rewrite !vassocl ; rewrite <- rwhisker_lwhisker ; rewrite !vassocr ; apply maponpaths_2 ; rewrite lwhisker_lwhisker ; rewrite !vassocl ; apply maponpaths ; rewrite !vassocr ; rewrite <- vcomp_whisker ; rewrite !vassocl ; apply maponpaths ; rewrite !vassocr ; rewrite <- lwhisker_lwhisker_rassociator ; rewrite !vassocl ; apply maponpaths ; rewrite !lwhisker_vcomp ; apply maponpaths ; exact (pr2 hα)). - intros x₁ x₂ x₃ f₁ f₂ g α hx₁ hx₂ hx₃ hf₁ hf₂ hg hα ; cbn in *. use make_disp_map_bicat_cell. + exact (pr1 hα ▹ _). + abstract (cbn ; rewrite !vassocl ; rewrite rwhisker_rwhisker ; rewrite !vassocr ; apply maponpaths_2 ; rewrite rwhisker_lwhisker ; rewrite !vassocl ; apply maponpaths ; rewrite <- vcomp_whisker ; rewrite !vassocr ; apply maponpaths_2 ; rewrite !vassocl ; rewrite <- rwhisker_rwhisker_alt ; rewrite !vassocr ; apply maponpaths_2 ; rewrite !rwhisker_vcomp ; apply maponpaths ; exact (pr2 hα)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.StreetFibration. 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.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration. Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration. Require Import UniMath.Bicategories.Logic.DisplayMapBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Codomain. Require Import UniMath.Bicategories.Limits.Pullbacks.