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) : transportb_square (id_right _) (id_right _) (lassociator_h h₁ h₂ (h₃ ·h h₄) ⋆v lassociator_h (h₁ ·h h₂) h₃ h₄) = (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. exact (pr22 (pr222 (pr222 C)) v w x y z h₁ h₂ h₃ h₄). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics.