Proposition composition_preserves_hor_comp_laws {C₁ C₂ C₃ : category} {D₁ : twosided_disp_cat C₁ C₁} {D₂ : twosided_disp_cat C₂ C₂} {D₃ : twosided_disp_cat C₃ C₃} {Cm₁ : hor_comp D₁} {Cm₂ : hor_comp D₂} {Cm₃ : hor_comp D₃} {F : C₁ ⟶ C₂} {G : C₂ ⟶ C₃} {FF : twosided_disp_functor F F D₁ D₂} (FFc : preserves_hor_comp Cm₁ Cm₂ FF) {GG : twosided_disp_functor G G D₂ D₃} (GGc : preserves_hor_comp Cm₂ Cm₃ GG) : preserves_hor_comp_laws (composition_preserves_hor_comp_data FFc GGc). Proof. intros x₁ x₂ y₁ y₂ z₁ z₂ vx vy vz h₁ k₁ h₂ k₂ s₁ s₂. cbn -[idtoiso_twosided_disp]. unfold composition_preserves_hor_comp_data. etrans. { apply maponpaths. apply idtoiso_twosided_disp_concat'. } rewrite two_disp_post_whisker_f. rewrite assoc_two_disp. unfold transportb_disp_mor2. rewrite transport_f_f_disp_mor2. rewrite idtoiso_twosided_disp_functor. rewrite two_disp_post_whisker_f. rewrite two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. rewrite twosided_disp_functor_comp_alt. rewrite two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. etrans. { apply maponpaths. apply maponpaths_2. apply maponpaths. apply is_natural_preserves_hor_comp. } rewrite transportf_twosided_disp_functor. rewrite two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. rewrite twosided_disp_functor_comp. unfold transportb_disp_mor2. rewrite two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. rewrite assoc_two_disp_alt. rewrite transport_f_f_disp_mor2. etrans. { do 2 apply maponpaths. apply is_natural_preserves_hor_comp. } rewrite two_disp_post_whisker_f. rewrite transport_f_f_disp_mor2. rewrite assoc_two_disp. unfold transportb_disp_mor2. rewrite transport_f_f_disp_mor2. rewrite idtoiso_twosided_disp_functor'. unfold transportb_disp_mor2. rewrite !two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. etrans. { apply maponpaths. apply maponpaths_2. apply idtoiso_twosided_disp_concat. } unfold transportb_disp_mor2. rewrite two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. use transportf_disp_mor2_eq. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TransportLaws. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics.