proposition: Proposition double_pentagon' {C : double_cat} {v w x y z : C} (h₁ : v -->h w) (h₂ : w -->h x) (h₃ : x -->h y) (h₄ : y -->h z) : lassociator_h h₁ h₂ (h₃ ·h h₄) ⋆v lassociator_h (h₁ ·h h₂) h₃ h₄ = transportf_square (id_right _) (id_right _) ((id_v_square h₁ ⋆h lassociator_h h₂ h₃ h₄) ⋆v lassociator_h h₁ (h₂ ·h h₃) h₄ ⋆v (lassociator_h h₁ h₂ h₃ ⋆h id_v_square h₄)).
proof: Proof. rewrite <- double_pentagon. rewrite transportfb_square. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics