English
When composing 2-squares in a grid, horizontal composition followed by vertical composition equals vertical composition followed by horizontal composition.
Русский
При объединении 2-углов в сетку, горизонтальное затем вертикальное композиционирование равно вертикальному затем горизонтальному.
LaTeX
$$$(w_1 \\; \\gg\\!\\!_h \\; w_2) \\; \\gg\\!\\!_v \\; (w_3 \\; \\gg\\!\\!_h \\; w_4) \\\\ = \\\\ (w_1 \\; \\gg\\!\\!_v \\; w_3) \\; \\gg\\!\\!_h \\; (w_2 \\; \\gg\\!\\!_v \\; w_4)$$$
Lean4
/-- When composing 2-squares which form a diagram of grid, composing horizontally first yields the
same result as composing vertically first. -/
theorem hCompVCompHComp (w₁ : TwoSquare T L R B) (w₂ : TwoSquare T' R R' B') (w₃ : TwoSquare B L' R'' B'')
(w₄ : TwoSquare B' R'' R₃ B₃) : (w₁ ≫ₕ w₂) ≫ᵥ (w₃ ≫ₕ w₄) = (w₁ ≫ᵥ w₃) ≫ₕ (w₂ ≫ᵥ w₄) :=
by
unfold hComp vComp whiskerLeft whiskerRight
ext c
simp only [comp_obj, NatTrans.comp_app, associator_hom_app, associator_inv_app, comp_id, id_comp, map_comp, assoc]
slice_rhs 2 3 => rw [← Functor.comp_map _ B₃, ← w₄.naturality]
simp
