English
Equivalences between the space of curried functions and the FromTypes representations are given by curry and uncurry, forming a natural equivalence.
Русский
Эквивалентности между пространством каррированных функций и представлениями FromTypes задаются карри и раскаррированием, образуя естественную эквивалентность.
LaTeX
$$$\\text{curryEquiv}(p,\\tau) : (((i:Fin\\ n) \\\\to p i) \\\\to \\tau) \\quad\\equiv\\quad \\mathrm{FromTypes}\; p\\tau$$$
Lean4
/-- `Equiv.curry` for `p`-ary heterogeneous functions. -/
@[simps]
def curryEquiv (p : Fin n → Type u) : (((i : Fin n) → p i) → τ) ≃ FromTypes p τ
where
toFun := curry
invFun := uncurry
left_inv := uncurry_curry
right_inv := curry_uncurry
