Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: currying

Christian Williams (May 10 2020 at 00:18):

I'm proving something that involves plenty of currying and uncurrying.
Right now I'm currying $f:a\times b\to c$ to $f^\bullet:a\to [b,c]$
and uncurrying $g:a\to [b,c]$ to $g^\circ:a\times b\to c$.

Is there a standard notation, or one that you think is good?

zigzag (May 10 2020 at 00:41):

These days I tend to write stuff like $\Lambda(f) : A \to C^B$ for currying, and $\Lambda^{-1}$ for uncurrying (which I seldom use, I have a bad tendency to use the more verbose $ev \circ (g \times id)$). I don't remember where I picked that up, but I think I like it because it reminds me of $\lambda$-abstraction, which is interpreted as currying in CCCs.

Nathanael Arkor (May 10 2020 at 01:27):

A common notation for curring is $\lambda f : a \to c^b$. Not sure about uncurrying, but $\lambda^{-1}$ seems reasonable.