currying₃ — Mathlib

English

There is an equivalence of categories between 3-variable functors and triple product functors, via currying

Русский

Существует эквивалентность категорий между трёхпеременными функторов и тройкой произведений через каррирование

LaTeX

$$$\text{currying₃} : (C_1 \to C_2 \to C_3 \to E) \simeq C_1 \times C_2 \times C_3 \to E$$$

Lean4

/-- The equivalence of categories `(C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ≌ C₁ × C₂ × C₃ ⥤ E`
given by the curryfication of functors in three variables. -/
def currying₃ : (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ≌ C₁ × C₂ × C₃ ⥤ E :=
  currying.trans (currying.trans (prod.associativity C₁ C₂ C₃).congrLeft)

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