Decategorifying multivariable adjunctions
Definition. An (n,m)-functional relation $R \colon (A_0,\dots,A_n) \to (B_0,\dots,B_m)$ is a relation $R \colon A_0 \times \dots \times A_n \to B_0 \times \dots \times B_m$ together with representing functions that, given an element of the relation missing exactly one element, return that exact element. That is, there exist functions $$f_j \colon A_0 \times \dots \times A_n \times B_0 \times \overset{\cancel{B_j}}\dots \times B_m \to B_j,$$ $$g_i \colon A_0 \times \overset{\cancel{A_i}}\dots \times A_n \times B_0 \times \dots \times B_m \to A_i,$$ such that $$R(a_0,\dots,b_m) \iff (f_j(a_0,\dots,b_m) = b_j) \iff (g_i(a_0,\dots,b_m) = a_i).$$
Example. The pair of functions witnessing a bijection constitutes a (1,1)-functional relation, $$(f(a) = b) \iff (g(b) = a).$$ In this sense, the categorification of inverse functions is adjoint functors.
Example. A (2,1) or (1,2)-relation is functional if we have three functions $f_0 \colon A_1 \times A_2 \to A_0$, $f_1 \colon A_2 \times A_0 \to A_1$ and $f_2 \colon A_0 \times A_1 \to A_2$ such that $$(f_0(a_1,a_2) = a_0) \iff (f_1(a_2,a_0) = a_1) \iff (f_2(a_0,a_1) = a_2).$$
Tags: multivariable adjunction