hComp_assoc_heq — Mathlib

English

The HEq version of the interchange associativity law holds: hComp (hComp η θ) κ is HEq to hComp η (hComp θ κ).

Русский

HEq-версия закона об обмене ассоциативности: hComp (hComp η θ) κ эквивалентно hComp η (hComp θ κ).

LaTeX

$$$HEq( hComp( hComp(\\eta, \\theta), \\kappa), hComp(\\eta, hComp(\\theta, \\kappa)))$$$

Lean4

theorem hComp_assoc_heq {a b c d : CatEnrichedOrdinary C} {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f')
    (θ : g ⟶ g') (κ : h ⟶ h') : HEq (hComp (hComp η θ) κ) (hComp η (hComp θ κ)) := by simp [hComp_assoc]

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