Decategorifying multivariable adjunctions

Definition. An (n,m)-functional relation $R:(A_0,\dots ,A_n)\to (B_0,\dots ,B_m)$ is a relation $R:A_0\times \cdots \times A_n\to B_0\times \cdots \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:A_0\times \cdots \times A_n\times B_0\times \stackrel{\cancel{B_j}}{\dots }\times B_m\to B_j,$ $g_i:A_0\times \stackrel{\cancel{A_i}}{\dots }\times A_n\times B_0\times \cdots \times B_m\to A_i,$ such that $R(a_0,\dots ,b_m)⟺(f_j(a_0,\dots ,b_m)=b_j)⟺(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)⟺(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:A_1\times A_2\to A_0$, $f_1:A_2\times A_0\to A_1$ and $f_2:A_0\times A_1\to A_2$ such that

(f_1(a_2,a_0) = a_1) \iff (f_2(a_0,a_1) = a_2).$$ Tags: [adjunction - multivariable adjunction](notes/pieces/adjunction%20-%20multivariable%20adjunction.md)