Proposition cell_are_companions_comp {B : verity_double_bicat} (H : vertically_saturated B) {x y : B} {h₁ h₂ h₃ : x --> y} (τ₁ : h₂ ==> h₁) (τ₂ : h₃ ==> h₂) {v₁ v₂ v₃ : x -|-> y} (c₁ : are_companions h₁ v₁) (c₂ : are_companions h₂ v₂) (c₃ : are_companions h₃ v₃) : cell_are_companions H (τ₂ • τ₁) c₁ c₃ = cell_are_companions H τ₁ c₁ c₂ • cell_are_companions H τ₂ c₂ c₃. Proof. unfold cell_are_companions. rewrite <- square_to_vertical_cell_comp. apply maponpaths. unfold comp_ver_globular_square. refine (!_). etrans. { do 2 apply maponpaths. rewrite <- lwhisker_hcomp_square. apply maponpaths. rewrite <- rwhisker_lwhisker_square. rewrite <- rwhisker_hcomp_square. apply idpath. } rewrite <- lwhisker_dwhisker_square. rewrite <- lwhisker_uwhisker_square. apply maponpaths. rewrite <- rwhisker_dwhisker_square. rewrite <- rwhisker_uwhisker_square. apply maponpaths. etrans. { do 2 apply maponpaths. etrans. { apply maponpaths_2. refine (!_). apply lunitor_v_comp_square''. } etrans. { apply maponpaths. refine (!_). apply runitor_v_comp_square''. } rewrite <- rwhisker_hcomp_square. apply maponpaths. rewrite rwhisker_lwhisker_square. rewrite <- lwhisker_hcomp_square. apply maponpaths. rewrite lrwhisker_hcomp_square. rewrite <- rwhisker_square_comp. rewrite r_rwhisker_v_comp_square. rewrite <- rwhisker_square_comp. rewrite !vassocr. rewrite vcomp_lunitor. rewrite !vassocl. rewrite runitor_rinvunitor. rewrite id2_right. rewrite l_lwhisker_v_comp_square. etrans. { apply maponpaths. apply maponpaths. apply lassociator_v_comp_square'. } rewrite <- lrwhisker_hcomp_square. rewrite <- !lwhisker_square_comp. etrans. { apply maponpaths. apply maponpaths_2. rewrite !vassocl. rewrite <- linvunitor_assoc. apply lunitor_linvunitor. } rewrite lwhisker_square_id. rewrite <- rwhisker_hcomp_square. apply maponpaths. rewrite double_bicat_interchange. rewrite double_bicat_interchange. rewrite l_dwhisker_h_comp_square. etrans. { apply maponpaths. apply maponpaths_2. apply maponpaths. apply are_companions_right'. } rewrite uwhisker_id_v_square. rewrite <- !dwhisker_square_comp. rewrite <- ud_whisker_vcomp_square. rewrite lunitor_v_comp_square'. apply idpath. } rewrite r_rwhisker_v_comp_square. rewrite <- !rwhisker_lwhisker_square. rewrite <- !rwhisker_square_comp. rewrite r_lwhisker_v_comp_square. rewrite <- !lwhisker_square_comp. etrans. { do 2 apply maponpaths. apply maponpaths_2. rewrite <- runitor_triangle. etrans. { apply maponpaths. rewrite !vassocr. rewrite lassociator_rassociator. apply id2_left. } rewrite runitor_lunitor_identity. rewrite lwhisker_vcomp. rewrite linvunitor_lunitor. apply lwhisker_id2. } rewrite rwhisker_square_id. etrans. { do 2 apply maponpaths. apply maponpaths_2. rewrite linvunitor_assoc. rewrite !vassocl. rewrite lunitor_lwhisker. rewrite runitor_lunitor_identity. rewrite rwhisker_vcomp. rewrite linvunitor_lunitor. apply id2_rwhisker. } rewrite lwhisker_square_id. rewrite ud_whisker_vcomp_square. etrans. { do 2 apply maponpaths. apply maponpaths_2. rewrite r_dwhisker_h_comp_square. rewrite <- !dwhisker_square_comp. apply maponpaths_2. rewrite !vassocr. rewrite vcomp_lunitor. rewrite !vassocl. rewrite rwhisker_hcomp. rewrite <- rinvunitor_natural. apply idpath. } rewrite dwhisker_vcomp_square. rewrite uwhisker_vcomp_square. rewrite <- !id_h_square_bicat_id. rewrite lunitor_h_comp_square'. rewrite runitor_h_comp_square'. rewrite <- !dwhisker_vcomp_square. rewrite <- uwhisker_vcomp_square. rewrite <- !dwhisker_square_comp. rewrite lunitor_runitor_identity. rewrite rinvunitor_runitor. rewrite dwhisker_square_id. rewrite dwhisker_uwhisker_square. rewrite <- uwhisker_vcomp_square. rewrite <- uwhisker_square_comp. rewrite linvunitor_lunitor. rewrite uwhisker_square_id. rewrite ud_whisker_vcomp_square. apply maponpaths_2. rewrite <- dwhisker_square_comp. apply maponpaths_2. rewrite !vassocl. rewrite rinvunitor_runitor. rewrite !id2_right. rewrite !vassocr. rewrite linvunitor_lunitor. rewrite id2_left. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.CellsAndSquares. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.CompanionPairs.