Proposition double_associator_nat {C : category} {D : twosided_disp_cat C C} {Cm : hor_comp D} (a : double_cat_associator Cm) {w₁ w₂ x₁ x₂ y₁ y₂ z₁ z₂ : C} {h₁ : D w₁ x₁} {h₂ : D w₂ x₂} {j₁ : D x₁ y₁} {j₂ : D x₂ y₂} {k₁ : D y₁ z₁} {k₂ : D y₂ z₂} {vw : w₁ --> w₂} {vx : x₁ --> x₂} {vy : y₁ --> y₂} {vz : z₁ --> z₂} (τ₁ : h₁ -->[ vw ][ vx ] h₂) (τ₂ : j₁ -->[ vx ][ vy ] j₂) (τ₃ : k₁ -->[ vy ][ vz ] k₂) : transportb_disp_mor2 (id_right _ @ !(id_left _)) (id_right _ @ !(id_left _)) (double_associator a h₁ j₁ k₁ ;;2 double_hor_comp_mor Cm (double_hor_comp_mor Cm τ₁ τ₂) τ₃) = double_hor_comp_mor Cm τ₁ (double_hor_comp_mor Cm τ₂ τ₃) ;;2 double_associator a h₂ j₂ k₂. Proof. apply (pr2 a). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos.