hComp_assoc — Mathlib

English

As a simplification, hComp (hComp η θ) κ equals hComp η (hComp θ κ) up to the same HEq used in the associativity statement.

Русский

Упрощённо, hComp (hComp η θ) κ равняется hComp η (hComp θ κ) в рамках той же формулировки HEq.

LaTeX

$$$ hComp\\left( hComp(\\eta,\\theta),\\kappa\\right) = hComp(\\eta, hComp(\\theta, \\kappa)) $$$

Lean4

theorem hComp_assoc {a b c d : CatEnriched C} {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f') (θ : g ⟶ g')
    (κ : h ⟶ h') : hComp (hComp η θ) κ = eqToHom (assoc f g h) ≫ hComp η (hComp θ κ) ≫ eqToHom (assoc f' g' h').symm :=
  by simp [← heq_eq_eq, hComp_assoc_heq]

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