Standard notation for the transform that turns a function $A \rightarrow (B \rightarrow C)$ into a function $B \rightarrow (A \rightarrow C).$

Question

Suppose we're given sets $A,B$ and $C$. Then to each function $f : A \rightarrow (B \rightarrow C)$, we can assign another function $F : B \rightarrow (A \rightarrow C)$ by defining:

$$F(b)(a) = f(a)(b)$$

Question. Is there standard notation for $F$, like $[f]$ or $\# f$ or something?

This is motivated by my question here; see the edit at the end of that question.

Answer 1

By request, making a comment into an answer.

In Computer Science this function is usually called flip, e.g., see here.

However, it is not that well known, and I would advise you to define it before usage, for example:

\begin{align} &\mathtt{flip}(f)(x)(y) &&= f(y)(x) &\text{classic style}\\ &\mathtt{flip}(f) &&= x \mapsto \big(y \mapsto f(y)(x)\big) &\text{'maps-to' style}\\ &\mathtt{flip} &&= \lambda f.\ \lambda x.\ \lambda y.\ f\ y\ x &\text{$\lambda$-calculus style}\\ &\mathtt{flip}\ f\ x\ y &&= f\ y\ x &\text{functional programming style} \end{align}

I hope this helps $\ddot\smile$

Answer 2

Well, besides $\operatorname{flip}$ there is $\operatorname{swap}$. This is the name used in the homotopy type theory book (see 1.4 and don't get confused by the dependent function types; it does what you want).