hComp_assoc_heq — Mathlib

English

For η : f ⟶ f', θ : g ⟶ g', κ : h ⟶ h', we have hComp (hComp η θ) κ = eqToHom (assoc f g h) ≫ hComp η (hComp θ κ) ≫ eqToHom (assoc f' g' h').symm.

Русский

Для η : f ⟶ f', θ : g ⟶ g', κ : h ⟶ h' выполняется hComp (hComp η θ) κ = eqToHom(assoc f g h) ≫ hComp η (hComp θ κ) ≫ eqToHom (assoc f' g' h').symm.

LaTeX

$$$ hComp\\left( hComp(\\eta,\\theta),\\kappa\\right) = eqToHom(assoc(f,g,h)) \\;≫\\; hComp(\\eta, hComp(\\theta,\\kappa)) \\;≫\\; eqToHom(assoc(f',g',h')).^{-1} $$$

Lean4

theorem hComp_assoc_heq {a b c d : CatEnriched C} {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f') (θ : g ⟶ g')
    (κ : h ⟶ h') : HEq (hComp (hComp η θ) κ) (hComp η (hComp θ κ)) :=
  congr_arg_heq (·.map (X := (_, _, _)) (Y := (_, _, _)) (η, θ, κ)) (e_assoc (V := Cat) a b c d)

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