curryingEquiv — Mathlib

English

The currying equivalence between bifunctors and curried functors is established

Русский

Установлена эквивалентность каррирования между бифунктором и каррированной формой функторов

LaTeX

$$$\text{curryingEquiv} : \mathsf{Fun}(C, \mathsf{Fun}(D, E)) \simeq \mathsf{Fun}(C \times D, E)$$$

Lean4

/-- The equivalence of types of bifunctors given by currying. -/
@[simps!]
def curryingEquiv : C ⥤ D ⥤ E ≃ C × D ⥤ E where
  toFun F := uncurry.obj F
  invFun G := curry.obj G
  left_inv := curry_obj_uncurry_obj
  right_inv := uncurry_obj_curry_obj

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