English
There is a dependent curry-uncurry equivalence between functions on a sigma type and functions of two arguments.
Русский
Существует зависимая эквивалентность карри-анкюри между функциями на сигма-типе и функциями двух аргументов.
LaTeX
$$$$ \\text{piCurry } : (\\forall x : \\Sigma i, \\beta i, \\gamma x.1 x.2) \\simeq (\\forall a, b, \\gamma a b). $$$$
Lean4
/-- Dependent `curry` equivalence: the type of dependent functions on `Σ i, β i` is equivalent
to the type of dependent functions of two arguments (i.e., functions to the space of functions).
This is `Sigma.curry` and `Sigma.uncurry` together as an equiv. -/
def piCurry {α} {β : α → Type*} (γ : ∀ a, β a → Type*) : (∀ x : Σ i, β i, γ x.1 x.2) ≃ ∀ a b, γ a b
where
toFun := Sigma.curry
invFun := Sigma.uncurry
left_inv := Sigma.uncurry_curry
right_inv := Sigma.curry_uncurry
