proposition: Proposition comp_are_companions_left : runitor (v₁ · v₂) ▹s (linvunitor (v₁ · v₂) ◃s ψ ⋆v φ) = id_h_square_bicat (v₁ · v₂).
proof: Proof. rewrite rwhisker_lwhisker_square. unfold φ, ψ. etrans. { apply comp_ul_dr_corner. } etrans. { apply maponpaths. apply maponpaths. etrans. { apply maponpaths. apply are_companions_left'. } apply maponpaths_2. apply are_companions_left'. } rewrite !l_rwhisker_v_comp_square. rewrite !r_rwhisker_v_comp_square. rewrite !l_lwhisker_v_comp_square. rewrite !r_lwhisker_v_comp_square. rewrite <- !rwhisker_square_comp. rewrite <- !lwhisker_square_comp. rewrite rwhisker_lwhisker_square. rewrite <- !lwhisker_square_comp. refine (_ @ lwhisker_square_id _ _). use eq_lwhisker_square. { rewrite !vassocl. etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite lunitor_triangle. apply idpath. } etrans. { apply maponpaths. rewrite !vassocr. rewrite vcomp_lunitor. rewrite !vassocl. rewrite lwhisker_vcomp. rewrite linvunitor_lunitor. rewrite lwhisker_id2. apply id2_right. } apply linvunitor_lunitor. } refine (_ @ rwhisker_square_id _ _). use eq_rwhisker_square. { etrans. { do 2 apply maponpaths. rewrite <- lwhisker_vcomp. rewrite !vassocr. rewrite lunitor_lwhisker. apply idpath. } etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite rinvunitor_runitor. rewrite id2_rwhisker. apply id2_left. } rewrite lwhisker_vcomp. rewrite rinvunitor_runitor. apply lwhisker_id2. } rewrite id_h_square_bicat_comp. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws UniMath.Bicategories.DoubleCategories.DoubleBicat.CellsAndSquares UniMath.Bicategories.DoubleCategories.DoubleBicat.UnderlyingCats UniMath.Bicategories.DoubleCategories.DoubleBicat.LocalUnivalence UniMath.Bicategories.DoubleCategories.Examples.TransposeDoubleBicat