proposition: Proposition l_dwhisker_h_comp_square {B : verity_double_bicat} {x₁ x₂ x₃ y₁ y₂ y₃ : B} {h₁ : x₁ --> x₂} {h₂ : x₂ --> x₃} {k₁ k₁' : y₁ --> y₂} {k₂ : y₂ --> y₃} {v₁ : x₁ -|-> y₁} {v₂ : x₂ -|-> y₂} {v₃ : x₃ -|-> y₃} (τ : k₁ ==> k₁') (s₁ : square_double_bicat h₁ k₁ v₁ v₂) (s₂ : square_double_bicat h₂ k₂ v₂ v₃) : (τ ▿s s₁) ⋆h s₂ = (τ ▹ k₂) ▿s (s₁ ⋆h s₂).
proof: Proof. rewrite rwhisker_hcomp. refine (!_). etrans. { use (hor_bicat_hcomp_h_comp_square B (id2 _) (id2 _) τ (id2 _)). - exact (τ ▿s s₁). - exact s₂. - rewrite uwhisker_square_id. apply idpath. - rewrite dwhisker_square_id, uwhisker_square_id. apply idpath. } rewrite hcomp_identity. rewrite uwhisker_square_id. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat