English
Horizontal and vertical compositions satisfy the interchange law: the horizontal composition of two vertical composites equals the vertical composition of the horizontal composites.
Русский
Горизонтальная и вертикальная композиции удовлетворяют закону взаимного обмена: горизонтальная композиция двух вертикальных композиций равна вертикальной композиции горизонтальных композиций.
LaTeX
$$$hComp(\\eta_1, \\theta_1) \\;\\gg\\; hComp(\\eta_2, \\theta_2) = hComp(\\eta_1 \\gg \\eta_2, \\theta_1 \\gg \\theta_2)$$$
Lean4
/-- The interchange law for horizontal and vertical composition of 2-cells in a bicategory. -/
@[simp]
theorem hComp_comp {a b c : CatEnrichedOrdinary C} {f₁ f₂ f₃ : a ⟶ b} {g₁ g₂ g₃ : b ⟶ c} (η : f₁ ⟶ f₂) (η' : f₂ ⟶ f₃)
(θ : g₁ ⟶ g₂) (θ' : g₂ ⟶ g₃) : hComp η θ ≫ hComp η' θ' = hComp (η ≫ η') (θ ≫ θ') := by
simp [hComp, ← CatEnriched.hComp_comp, Hom.comp_eq]
