hComp_comp — Mathlib

English

For every a, the left and right unitors at the identity on a give the same hom component: (λ_(1 a)).hom = (ρ_(1 a)).hom.

Русский

Для каждого объекта a левые и правые униторы над 1_a имеют одинаковый гом-компонент: (λ_(1 a)).hom = (ρ_(1 a)).hom.

LaTeX

$$$ (\\lambda_{(1 a)}).hom = (\\rho_{(1 a)}).hom $$$

Lean4

/-- The interchange law for horizontal and vertical composition of 2-cells in a bicategory. -/
@[simp]
theorem hComp_comp {a b c : CatEnriched C} {f₁ f₂ f₃ : a ⟶ b} {g₁ g₂ g₃ : b ⟶ c} (η : f₁ ⟶ f₂) (η' : f₂ ⟶ f₃)
    (θ : g₁ ⟶ g₂) (θ' : g₂ ⟶ g₃) : hComp η θ ≫ hComp η' θ' = hComp (η ≫ η') (θ ≫ θ') :=
  ((eComp Cat a b c).map_comp (Y := (_, _)) (_, _) (_, _)).symm

Похожие утверждения