hComp_id_heq — Mathlib

English

Given η : f ⟶ f', θ : g ⟶ g', κ : h ⟶ h', the horizontal composition is associative up to HEq: HEq (hComp (hComp η θ) κ) (hComp η (hComp θ κ)).

Русский

При η : f ⟶ f', θ : g ⟶ g', κ : h ⟶ h' горизонтальная композиция ассоциируется в терминах HEq: HEq (hComp (hComp η θ) κ) (hComp η (hComp θ κ)).

LaTeX

$$$ HEq\\left( \\mathrm{hComp}(\\mathrm{hComp}(\\eta,\\theta), \\kappa) , \\mathrm{hComp}(\\eta, \\mathrm{hComp}(\\theta, \\kappa))\\right) $$$

Lean4

theorem hComp_id_heq {a b : CatEnriched C} {f f' : a ⟶ b} (η : f ⟶ f') : HEq (hComp η (𝟙 (𝟙 b))) η :=
  by
  rw [id_eq, ← Functor.map_id]
  exact congr_arg_heq (·.map η) (e_comp_id (V := Cat) a b)

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