Dependent curry

Stream: Is there code for X?

[Nir Paz]

Do we have something like this?

def Equiv.sigma_arrow {ι : Type*} (α : Type*) (f : ι → Type*) :
    (Sigma f → α) ≃ ((i : ι) → f i → α)

If not, is there a better name for it?

[Daniel Weber]

@loogle Sigma, Equiv

[loogle]

:search: Equiv.sigmaEquivProd, Equiv.sigmaPLiftEquivSubtype, and 200 more

[Daniel Weber]

docs#Equiv.piCurry

[Nir Paz]

Thanks!