Proposition comp_are_companions_left : runitor (v₁ · v₂) ▹s (linvunitor (v₁ · v₂) ◃s ψ ⋆v φ) = id_h_square_bicat (v₁ · v₂). 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.
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.Univalence. Require Import UniMath.Bicategories.Core.BicategoryLaws. 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.UnderlyingCats. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.LocalUnivalence. Require Import UniMath.Bicategories.DoubleCategories.Examples.TransposeDoubleBicat.