The Zappa-Szép product, strict factorization systems and distributive laws

$\newcommand{\con}{\mathbf{Set}} \newcommand{\uno}{\mathbf{1}} \newcommand{\Cat}{\mathbf{Cat}}\newcommand{\mon}{\mathbf{Mon}} \newcommand{\ab}{\mathbf{Ab}} \newcommand{\an}{\mathbf{An}}\newcommand {\matcon}{\mathbf{Set\text{-}Mat}} \newcommand{\grp}{\mathbf{Grp}} \newcommand{\ob}{\mathrm{Ob}}$

The Zappa-Szép product and distributive laws

The Zappa-Szép product, strict factorization systems and distributive laws are related in a certain way. Let us talk first about the Zappa-Szép product (also known as knit product or matched pair of groups).
     The Zappa-Szép product is a generalization of the semidirect product for groups in the same way as this product is a generalization of the direct product for groups, and the zappa-szép product is the most general way in which a group is presented as a product of two groups.
     The internal Zappa-Szép product is defined as follows. Given a group $G$ and two subgroups $H$ and $K$ of $G$, the following statements are equivalent:

• $G=KH$ y $K\cap H=\{e\}$,
• for every $g\in G$ there is a unique $k\in K$ and a unique $h\in H$ such that $g=kh$.

If either of these statements is satisfied, then $G$ is said to be an internal Zappa-Szép product of $K$ and $H$.
     There is an external version of the Zappa-Szép product, which is the one we are interested in, because it's by means of this product that a link between distributive laws and strict factorization systems is established.
     Given two groups $K$ and $H$, suppose there are funtions $\alpha:H\times K\rightarrow K$ and $\beta:H\times K\rightarrow H$ such that

1. $\alpha(h_1h_2,k)=\alpha(h_1,\alpha(h_2,k))$,
2. $\beta(h_1h_2,k)=\beta(h_1,\alpha(h_2,k))\beta(h_2,k)$,
3. $\beta(h,k_1k_2)=\beta(\beta(h,k_1),k_2)$,
4. $\alpha(h,k_1k_2)=\alpha(h,k_1)\alpha(\beta(h,k_1),k_2)$,
5. $\alpha(e,k)=k$,
6. $\beta(h,e)=h$

for every $h,h_1,h_2\in H$ y $k,k_1,k_2\in K$ (cf. [4]). Note that from (ii) and (v) and from (iv) and (vi) follows respectively:

7. $\beta(e,k)=e$ and
8. $\alpha(h,e)=e$.

We can define from (i)-(vi) a multiplication and an inverse on $K\times H$ as $$(k_1,h_1)\gamma(k_2,h_2):=(k_1\alpha(h_1,k_2),\beta(h_1,k_2)h_2))$$ and $$(k,h)^{-1}:=(\alpha(h^{-1},k^{-1}),\beta(h^{-1},k^{-1})).$$ $(\gamma,K\times H)$ is called an external Zappa-Szép product of $K$ and $H$.
     Note that if $G$ is an internal Zappa-Szép product of its subgroups $K$ y $H$, then there are funtions $\alpha:H\times K\rightarrow K$ and $\beta:H\times K\rightarrow H$ such that (i), (ii), (iii), (iv), (v) and (vi) in the previous definition are satisfied: their existence follows from the fact that every element $g\in G$ can be written uniquely as a product $kh$, and the fact that if $G$ is an external Zappa-Szép product of the groups $K$ and $H$, then $G$ is an internal Zappa-Szép product of its subgroups $K\times e_H$ and $e_K\times H$.
     Let $H,K\in\grp$. Let $S$ and $T$ be the endofunctors $H\times(-)$ and $K\times(-)$ on $\con$, respectively. Then we have the monads $$H\times X,\quad\xymatrix{X\ar[r]^(.4){e_H\times 1_X} & H\times X},\quad\xymatrix{H\times H\times X\ar[r]^(.6){m_H\times 1_X} & H\times X}$$ and $$K\times X,\quad\xymatrix{X\ar[r]^(.4){e_K\times 1_X} & K\times X},\quad\xymatrix{K\times K\times X\ar[r]^(.6){m_K\times 1_X} & K\times X}.$$ Denote their units and multiplicationss as $\eta',\mu'$ y $\eta,\mu$, resp. Let $\gamma$ be a group structure on $K\times H$ such that $K\times e_H,e_K\times H$ are subgroups of $(\gamma,K\times H)$ and $(K\times e_H)\gamma(e_K\times H)=(\gamma,K\times H)$. In other words, such that $(\gamma,K\times H)$ is an internal Zappa-Szép product of $K\times e_H$ and $e_k\times H$, or that $(\gamma, K\times H)$ is an external Zappa-Szép product of $K$ and $H$.
     Without loss of generality, we can assume $(k,h)=(k,e_H)\gamma(e_K,h)$ for any $k\in K$ and $h\in H$ (consider the definition of external Zappa-Szép product and the properties of $\alpha$ and $\beta$). Then we have the monad $$(K\times H\times(-),(e_K,e_H)\times 1_{(-)}, \gamma\times 1_{(-)})$$ on $\con$. Since $K\times e_H$ and $e_K\times H$ are subgroups of $(\gamma,K\times H)$, then $\eta S$ and $T\eta'$ are morphisms of monads, and since $(k,h)=(k,e_H)\gamma(e_K,h)$, the previous monad satisfies the middle unitary law, so the monad above induces a distributive law $ST\Rightarrow TS$; namely, $$(\gamma\times 1_{(-)})\cdot\eta ST\eta':H\times K\times(-)\Rightarrow K\times H\times(-);$$ explicitly, $$\xymatrix{(h,k,-)\ar@{|->}[r] & (e_K,h,k,e_H,-)\ar@{|->}[r] & ((e_K,h)\gamma(k,e_H),-)}.$$
     Conversely, let $\lambda:ST\Rightarrow TS$ be a distributive law of $S$ over $T$, and consider $\lambda 1:H\times K\times 1\rightarrow K\times H\times 1$. Neglect the singleton, and put $$\lambda 1=(\alpha,\beta),$$ where $\alpha$ and $\beta$ are determined by the following commutative diagram: $$\xymatrix{ & H\times K\ar[d]^{\lambda 1}\ar[dr]^\alpha\ar[dl]_\beta &\\ K & K\times H\ar[l]^{p_K}\ar[r]_{p_H} & H. }$$ Then, by the compatibility of $\lambda$ with the unit of $S$, $$\xymatrix{ & H\times K\times 1\ar[dd]^{\lambda 1}\\ K\times 1\ar[ur]^{e_H\times K\times 1}\ar[dr]_{K\times e_H\times 1} &\\ & K\times H\times 1 }$$ commutes; hence, $\alpha(e_H,k)=k$ y $\beta(e_H,k)=e_H$.
     Now, by the compatibility of $\lambda$ with the multiplication of $S$, $$\xymatrix{ H\times H\times K\times 1\ar[rr]^{H\times\lambda 1}\ar[d]_{m_H\times K\times 1} & & H\times K\times H\times 1\ar[rr]^{\lambda_{H\times 1}} & & K\times H\times H\times 1\ar[d]^{K\times m_H\times 1}\\ H\times K\times 1\ar[rrrr]_{\lambda 1} & & & & K\times H\times 1 }$$ commutes; whence, $$\alpha(h_1h_2,k)=\alpha(h_1,\alpha(h_2,k))\quad\text{y}\quad \beta(h_1h_2,k)=\beta(h_1,\alpha(h_2,k))\beta(h_2,k).$$ Similarly, by the compatibility of $\lambda$ with the unit and the multiplication of $T$, $\alpha(h,e_K)=e_K$, $\beta(h,e_K)=h$ and $$\alpha(h,k_1k_2)=\alpha(h,k_1)\alpha(\beta(h,k_1),k_2)\quad\text{y}\quad\beta(h,k_1k_2)=\beta(\beta(h,k_1),k_2).$$
     Therefore, we have a Zappa-Szép product of $K$ and $H$.
     Thus we have a correspondence between the Zappa-Szép products of $K$ and $H$, and the distributive laws of $H\times(-)$ over $K\times(-)$. Indeed, define $L:\mathbf{Zappa\text{-}Sz\acute{e}p}(K,H)\rightarrow\mathbf{DistLaw}(H,K)$, a function which goes from the Zappa-Szép products of $K$ and $H$ to the distributive laws of $H\times(-)$ ovoer $K\times(-)$ (let $\alpha:H\times K\rightarrow K$ and $\beta:H\times K\rightarrow H$ be the functions which define a Zappa-Szép product of $K$ and $H$): $$\xymatrix{ \mathbf{Zappa\text{-}Sz\acute{e}p}(K,H)\ar[r]^(.55)L & \mathbf{DistLaw}(H,K) }\qquad\qquad\quad$$ $$\xymatrix{ (\alpha,\beta)\ar@{|->}[r] & (\alpha,\beta)\times 1_{(-)}. }$$ Define $N:\mathbf{DistLaw}(H,K)\rightarrow\mathbf{Zappa\text{-}Sz\acute{e}p}(K,H)$ as $$\xymatrix{ \mathbf{DistLaw}(H,K)\ar[r]^(.45)N & \mathbf{Zappa\text{-}Sz\acute{e}p}(K,H) }\qquad\qquad\quad$$ $$\xymatrix{ \lambda\ar@{|->}[r] & (p_K\circ\lambda 1,p_H\circ\lambda 1). }$$ Obviously $NL=1$. Less obvious is that $LN=1$. Since $\con$ is a distributive category, \begin{equation}\label{D:distcatset} Z\times X=\sum\nolimits_{x\in X}Z\times H\times\{x\}. \end{equation}
     Consider now the injection $i_x:\{x\}\rightarrow X$; then by naturality of $\lambda$, the following diagram commutes: $$\xymatrix{ H\times K\times\{x\}\ar[rr]^{H\times K\times i_x}\ar[d]_{\lambda_{\{x\}}} & & H\times K\times X\ar[d]^{\lambda_X}\\ K\times H\times\{x\}\ar[rr]_{K\times H\times i_x} & & K\times H\times X. }$$ On the other hand, since $H\times K\times i_x$ is the injection $$\xymatrix{H\times K\times\{x\}\ar[r] & \sum_{x\in X}H\times K\times\{x\}},$$ $K\times H\times i_x$ is the injection $$\xymatrix{K\times H\times\{x\}\ar[r] & \sum_{x\in X}K\times H\times\{x\}}$$ and the equality \eqref{D:distcatset} holds, $\lambda_X=\sum_{x\in X}\lambda_{\{x\}}$. However $\lambda_{\{x\}}=\lambda 1\times 1_{\{x\}}$ for every $x\in X$, so $\lambda_X=\lambda 1\times 1_X$. Hence, $\lambda_X=(p_K\circ\lambda 1,p_H\circ\lambda 1)\times 1_X$.

The bicategory of set-valued matrices

The Zappa-Szép product is generalized in [3] by showing the equivalence of the concept of distributive law in the bicategory of set-valued matrices and the concept of strict factorization system. Let's see how that is done. First describe the bicategory of set-valued matrices $\matcon$ as follows: the objects (the 0-cells) of $\matcon$ are sets, a 1-cell $M:A\rightarrow B$ is a set-valued matrix, i. e., $M(b,a)\in\con$ for every $a\in A$ and $b\in B$, a 2-cell $\tau:M\Rightarrow N:A\rightarrow B$ is a matrix of functions $\tau(b,a):M(b,a)\rightarrow N(b,a)$. The composite of 1-cells $$\xymatrix{ A\ar[r]^M & B\ar[r]^E & C\ar@{}|{=}[r] & A\ar[r]^{EM} & C }$$ is defined as $$EM(c,a):=\sum_{a\in A}E(c,b)\times M(b,a).$$ Given $A\in\matcon$, we define $$1_A(b,a):= \begin{cases} 1,\text{ the singleton, if $b=a$};\\ \emptyset,\text{ if $b\neq a$}. \end{cases}$$ It is clear that $M 1_A\overset{r}{\cong} M$ and $1_B M\overset{l}{\cong} M$.
     A monad $T$ on an object $A$ in this bicategory is precisely a category with set of objects $A$. Let's shed some light on what is happening. Diagrammatically $T$ is determined by the following commutative diagrams: $$\xymatrix{ (TT)T\ar@{}|{\cong}[r]\ar[d]_{\mu T} & T(TT)\ar[r]^(.55){T\mu} & TT\ar[d]^\mu\\ TT\ar[rr]_\mu & & T }$$ and $$\xymatrix{ 1_AT\ar[r]^{\eta T}\ar[dr]_l & TT\ar[d]^\mu & T1_A\ar[l]_{T\eta}\ar[ld]^r\\ & T &, }$$ where $l$ and $r$ are the isomorphisms above induced by the product and the terminal object of $\con$. Now, what $T$ does is to assign to each pair of elements $b,a\in A$ a set $T(b,a)$ of arrows, to give a composite to each composable pair by means of $\mu$, to choose an identity for each element $a\in A$ via $\eta$ and finally, with the previous diagrams, to make composition associative and make composition with an identity a unit law for the arrows of the small category $A$ with objects its elements and its arrows in $T(b,a)$; put differently, a monad in $\matcon$ is a category.
     Now let $M$ and $E$ be two categories with set of objects $A$ and let $\lambda:ME\Rightarrow EM$ be a distributive law of $M$ over $E$; $\lambda$ yields a function $$\xymatrix{ ME(a,c)\ar[r]^{\lambda(a,c)} & EM(a,c) }$$ for every pair $(a,c)\in A\times A$. Thus we have a family of functions $$(\xymatrix{ M(a,b)\times E(b,c)\ar[r] & \sum_{i\in A}E(a,i)\times M(i,c) })_{b\in A}.$$ If we write $m:\xymatrix{a\ \ar@{>->}[r] & b}$ for an arrow in $M$ and $e:\xymatrix{b\ar@{->>}[r] & c}$ for an arrow in $E$, then $\lambda$ yields an object $e_\lambda m$ and a composable pair $(e_\alpha m,e_\beta m)$ as shown by: $$\xymatrix{ a\; \ar@{>->}[r]^m\ar@{->>}[d]_{e_\alpha m}\ar@{}|{\triangleleft\scriptscriptstyle{\dashv}}[dr] & b\ar@{->>}[d]^e\\ e_\lambda m\;\ar@{>->}[r]_{e_\beta m} & c. }$$ We call a diagram such as this a $\lambda$-square. Consider the compatibility diagrams for the distributive law $\lambda:ME\Rightarrow EM$: \begin{equation} \vcenter{\xymatrix{ & ME\ar[dd]^\lambda\\ E\ar[ru]^{1E}\ar[dr]_{E1} & \\ & EM, }}\quad\text{compatibility of $\lambda$ with $1$ (CuM)}\notag \end{equation} \begin{equation} \vcenter{\xymatrix{ & ME\ar[dd]^\lambda\\ M\ar[ur]^{M1}\ar[dr]_{1 M} &\\ & EM, }}\quad\text{compatibility of $\lambda$ with $1$ (CuE)}\notag \end{equation} \begin{equation} \vcenter{\xymatrix{ MME\ar[r]^{M\lambda}\ar[d]_{\bullet E} & MEM\ar[r]^{\lambda M} & EMM\ar[d]^{E\bullet}\\ ME\ar[rr]_\lambda & & EM, }}\quad\text{compatibility of $\lambda$ with $\bullet$ (CmM)}\notag \end{equation} \begin{equation} \vcenter{\xymatrix{ MEE\ar[r]^{\lambda E}\ar[d]_{M\bullet} & EME\ar[r]^{E\lambda} & EEM\ar[d]^{\bullet M}\\ ME\ar[rr]_\lambda & & EM, }}\quad\text{compatibility of $\lambda$ with $\bullet$ (CmE)}\notag \end{equation} where we denote by 1 the transformations that provide identities and by $\bullet$ the transformations that provide the composites (the units and the multiplications of the monads $M$ and $E$). Now, in terms of $\lambda$-squares, the compatibility of $\lambda$ with the units is expressed by $$\xymatrix{ b\;\ar@{>->}[r]^{1_b}\ar@{->>}[d]_e\ar@{}|{\triangleleft\scriptscriptstyle{\dashv}}[dr] & b\ar@{->>}[d]^e & & a\;\ar@{>->}[r]^m\ar@{->>}[d]_{1_a}\ar@{}|{\triangleleft\scriptscriptstyle{\dashv}}[dr] & b\ar@{->>}[d]^{1_b}\\ c\;\ar@{>->}[r]_{1_c} & c & & a\;\ar@{>->}[r]_m & b; }$$ i. e., CuM and CuE state that ${1_b}_\lambda e=c,m_\lambda 1_b=a$ and that

1. ${1_b}_\alpha e=e$,
2. ${1_b}_\beta e=1_c$,
3. $m_\alpha 1_b=1_a$,
4. $m_\beta 1_b=m$.

Chasing the upper right path of the diagram of CmM yields $$\xymatrix{ a\;\ar@{>->}[rr]^m\ar@{->>}[d]_{m_\alpha(n_\alpha e)}\ar@{}|{\triangleleft\scriptscriptstyle{\dashv}}[drrrr] & & b\;\ar@{>->}[rr]^n & & b''\ar@{->>}[d]^e\\ m_\lambda(n_\alpha e)\;\ar@{>->}[rr]_{m_\beta(n_\alpha e)} & & n_\lambda e\;\ar@{>->}[rr]_{n_\beta e} & & c; }$$ chasing the left lower path, $(mn)_\lambda e=m_\lambda(n_\alpha e)$ and

5. $(mn)_\alpha e=m_\alpha(n_\alpha e)$,
6. $(mn)_\beta e=m_\beta(n_\alpha e)\bullet n_\beta e$.

Similarly, for CmE, if we chase the upper right paht of the diagram, then $$\xymatrix{ a\;\ar@{>->}[rr]^m\ar@{->>}[d]_{m_\alpha e}\ar@{}|{\triangleleft\scriptscriptstyle{\dashv}}[ddrr] & & b\;\ar@{->>}[d]^e\\ m_\lambda e\ar@{->>}[d]_{(m_\beta e)_\alpha f} & & b'\ar@{->>}[d]^f\\ (m_\beta e)_\lambda f\;\ar@{>->}[rr]_(.55){(m_\beta e)_\beta f} & & c; }$$ chasing the left lower path, $m_\lambda(ef)=(m_\beta e)_\lambda f$ and

7. $m_\alpha(ef)=m_\alpha e\bullet(m_\beta e)_\alpha f$,
8. $m_\beta(ef)=(m_\beta e)_\beta f$.

If $A$ has a single element, then $M$ and $E$ are monoids, the equations (I)-(VIII) are the equations (i)-(viii) and the equalities for objects are trivial.
     From the general theory of distsributive law [1], $\lambda$ induces a composite monad $E_\lambda M$, a category with set of objects $A$ in which an arrow from $a$ to $c$ is given by specifying a third object $b$ and a pair $$\xymatrix{ a\ar@{->>}[r]^e & b\;\ar@{>->}[r]^m & c }$$ with $e$ in $E$ and $m$ in $M$; i. e., the arrows in $E_\lambda M$ are described as a formal composition $e\circ m$. The composition in $E_\lambda M$ is given by the multiplication for the monad $E_\lambda M$; namely, by $$\xymatrix{ & & EEM\ar[dr]^{\bullet M} & \\ EMEM \ar[r]^{E\lambda M} & EEMM\ar[ur]^{EE\bullet}\ar[dr]_{\bullet MM}\ar[rr]^(.55){\bullet\;\bullet} & & EM\\ & & EMM\ar[ur]_{E\bullet} &, }$$ thus the composite of $a\overset{e}{\twoheadrightarrow} b\overset{m}{\rightarrowtail} c$ and $c\overset{f}{\twoheadrightarrow} d\overset{n}{\rightarrowtail} x$ is given by $$\xymatrix{ a\ar@{->>}[r]^e\ar@{->>}[dr]_{e\bullet m_\alpha f} & b\;\ar@{>->}[r]^m\ar@{->>}[d]_(.35){m_\alpha f}\ar@{}|{\triangleleft\scriptscriptstyle{\dashv}}[dr] & c\ar@{->>}[d]^f\\ & m_\lambda f\;\ar@{>->}[r]_(.6){m_\beta f}\ar@{>->}[dr]_{m_\beta f\bullet n} & d\ar@{>->}[d]^n\\ & & x; }$$ i. e., $(e\circ m)\bullet(f\circ n)=(e\bullet m_\alpha f)\circ(m_\beta f\bullet n)$.
     It is easy to check that the unit of the composite monad $E_\lambda M$ characterizes the identities in $E_\lambda M$ by $$a\overset{1_a}{\twoheadrightarrow}a\overset{1_a}{\rightarrowtail}a.$$
     The morphisms of monads $1M:M\rightarrow E_\lambda M$ and $E1:E\rightarrow E_\lambda M$ are given by $m\mapsto 1\circ m$ and $e\mapsto e\circ 1$, resp. The middle unitary law yields that for every $e\circ m$ in $E_\lambda M$, $$(e\circ 1)\bullet(1\circ m)=e\circ m$$ holds.
     Note that if $M$ and $E$ are monoids, the composition in $E_\lambda M$ is the multiplication defined in the case of the Zappa-Szép product for groups.
     There is a greater generalization of the Zappa-Szép product in [2]; however, things there are done more à la Ehresmann.

Strict factorization systems

Given a category $C$ with $\ob(C)=:A$, a strict factorization system on $C$ is a pair of subcategories $S:=(E,M)$ of $C$ such that $\ob(M)=\ob(E)=\ob(C)$ and such that for every $f$ in $C$, there is a unique factorization $f=e_fm_f$ with $e_f$ in $E$ and $m_f$ in $M$. Consider $M$ and $E$ as monads on $A$ in $\matcon$. The pair $(E,M)$ induces a distributive law $\lambda_S:ME\Rightarrow EM$; indeed, define $\lambda_S$ by $$\xymatrix{ ME\ar[r]^{\lambda_S} & EM }$$ $$\xymatrix{ a\ar[r]^n & b\ar[r]^f & c\ar@{|->}[r] & a\ar[r]^{e_{n\cdot f}} & i\ar[r]^{m_{n\cdot f}} & c. }\ $$ Its compatibility with the unit of $M$ is obvious, for $m\cdot 1_b=m$. Now, the upper right path of the compatibility diagram of $\lambda_S$ with respect to the multiplication of $M$ (check the diagram above) produces the following diagram: $$\xymatrix{ a\ar[rr]^f\ar[dr]_{e_{f\cdot e_{g\cdot h}}} & & b\ar[r]^g\ar[dr]_(.45){e_{g\cdot h}} & c\ar[r]^h & d\\ & k\ar[rr]_{m_{f\cdot e_{g\cdot h}}} & & j\ar[ur]_{m_{g\cdot h}} &\ ; }$$ so $f\cdot g\cdot h$ has as factorization $e_{f\cdot e_{g\cdot h}}\cdot m_{f\cdot e_{g\cdot h}}\cdot m_{g\cdot h}$, which is unique; whence, the left lower path in the compatibility diagram of $\lambda_S$ with respect to the multiplication of $M$ produces the same result, and in consequence the compatibility of $\lambda_S$ with $M$ is satisfied. Similarly, the compatibility of $\lambda_S$ with $E$ is satisfied.
     Conversely, let $\lambda:ME\Rightarrow EM$ be a distributive law in $\matcon$, and consider the subcategories of $E_\lambda M$ defined by $$\lambda E:=\{e\circ 1\mid e\in E\}\quad\text{y}\quad M\lambda:=\{1\circ m\mid m\in M\}.$$ Each of these subcategories contains all the identities of $E_\lambda M$ and thus each contains all the objects of $E_\lambda M$. By the middle unitary law, $e\circ m$ is factorized as $(e\circ 1)\bullet(1\circ m)$. It is clear that this factorization is unique, and therefore $(\lambda E, M\lambda)$ is a strict factorization system $S_\lambda$ for $E_\lambda M$.
     We leave this correspondence just right there; i. e., we won't show that $S_{(-)}$ and $\lambda_{(-)}$ are biequivalences inverse of each other, because this is not our objetive right now.
     The way a distributive law is induced by the Zappa-Szép product in the group case makes us wonder whether a distributive law in $\matcon$ participates in a correspondence of that kind...

References

[1] Beck, J. [1969]: Distributive laws, Seminar on Triples and Categorical Homological Theory, ETH 1966/67, 80, 119-140 (1969). ↩
[2] Brin, M. G. [2005]: On the Zappa-Szép Product, Communications in Algebra, 33, 393-424 (2005). ↩
[3] Rosebrugh, R., Wood, R. J. [2002]: Distributive laws and factorization, Journal of Pure and Applied Algebra, 175(1-3), 327-353 (2002). ↩
[4] Takeuchi, M. [1981]: Matched pairs of groups and bismash products of Hopf algebras, Communications in Algebra, 9(8), 841-882 (1981). ↩

Coálgebras, coinducción y computación, una brevísima introducción

Ya hace varias décadas que las estructuras de datos trataron de describirse de manera algebraica, y con éxito varias de ellas. Sin embargo, hay otras estructuras de datos que no pueden describirse algebraicamente de manera apropiada. Con el tiempo, comenzó a entenderse que tales estructuras quedaban mejor modeladas coalgebraicamente, como las estructuras que implican una noción de estado que puede cambiar; por ejemplo, los sistemas de transición, los autómatas, la semántica de programación orientada a objetos, los automorfismos parciales, los números reales, las listas infinitas, las series de potencias formales, etc.
     Volviendo a las álgebras, desde el punto de vista del álgebra universal, se tiene que las signaturas de operaciones inducen ciertos funtores polinomiales y que las álgebras de estos funtores corresponden a las álgebras o modelos de las signaturas. Si generalizamos, dado un funtor $F:\mathbf{Con}\rightarrow\mathbf{Con}$, un álgebra de $F:\mathbf{Con}\rightarrow\mathbf{Con}$ (o una $F$-álgebra) es un par $(B,\beta:FB\rightarrow B)$, donde $B\in\mathbf{Con}$ y $\beta$ es una función. Dualmente, una coálgebra de $F$ (o una $F$-coálgebra) es un par $(A,\alpha:A\rightarrow FA)$, con $A\in\mathbf{Con}$ y $\alpha$ una función.
     Ahora, la inducción, como principio para definir o demostrar, se utiliza para las estructuras algebraicas que son generadas por una colección de constructores (u operaciones constructoras) —como los números naturales, que son generados por $0:1\rightarrow\mathbb{N}$ y $s:\mathbb{N}\rightarrow\mathbb{N}$, o como las listas y los árboles finitos—. Estas estructuras algebraicas son las álgebras iniciales en la categoría de álgebras de algún funtor pertinente; más precisamente, el principio de inducción en una estructura, como en el conjunto de los números naturales $\mathbb{N}$ o en el conjunto de las listas finitas $A^\ast$ sobre $A$, puede reformularse como la inicialidad de esa estructura en la categoría de álgebras de algún funtor. Dualmente, la terminalidad en la categoría de coálgebras de un funtor nos da un principio de coinducción para la cóalgebra terminal (o final) de esa categoría. La coálgebra terminal viene equipada con destructores u operaciones destructoras (también llamadas observadores, accesores, mapeos de transición o mutadores), las cuales la cogeneran. Volviendo a la inducción y siguiendo con la correspondencia entre inducción y la inicialidad, esta implica existencia única: la existencia corresponde a definir por inducción y la unicidad a demostrar por inducción. Tal correspondencia también se tiene para la coinducción.
     La coinducción puede formularse de manera alternativa mediante el concepto de bisimulación, que es una relación sobre una coálgebra que es cerrada de manera apropiada bajo las operaciones coalgebraicas de la coálgebra; tales relaciones se pueden entender como el concepto dual de congruencia, que es una relación cerrada bajo operaciones algebraicas.
     Volviendo a las álgebras, expliquemos de manera más precisa la correspondencia entre álgebras de una signatura y las álgebras de funtores polinomiales. Sea $\Sigma$ una signatura (monoespécica), así que, dada una $\Sigma$-álgebra $X$ y $\sigma\in\Sigma$, se tiene una operación $$\sigma_X:\underbrace{X\times\cdots\times X}_{\mathrm{ar}(\sigma)\text{ veces}}\rightarrow X,$$ donde $\mathrm{ar}(\sigma)$ es la aridad de $\sigma$. Así que si $\Sigma=\{\sigma_1,\ldots,\sigma_n\}$, podemos asociarle a $\Sigma$ el funtor $T_\Sigma:\mathbf{Con}\rightarrow\mathbf{Con}$ dado como $$T_\Sigma X:=X^{\mathrm{ar}(\sigma_1)}+\cdots +X^{\mathrm{ar}(\sigma_n)}.$$ Ahora, la estructura algebraica $\beta:T_\Sigma X\rightarrow X$ de un álgebra $X$ del funtor $T_\Sigma$ puede identificarse con una $n$-cotupla $$\beta=[\beta_1,\ldots,\beta_n]:X^{\mathrm{ar}(\sigma_1)}+\cdots +X^{\mathrm{ar}(\sigma_n)}\rightarrow X$$ de funciones $\beta_i:X^{\mathrm{ar}(\sigma_i)}\rightarrow X$. De aquí, las álgebras de $T_\Sigma$ corresponden a los modelos de $\Sigma$, las $\Sigma$-álgebras. Es decir, los funtores polinomiales construidos a partir del funtor identidad, productos y coproductos tienen como álgebras las álgebras que son modelos de signaturas. Un ejemplo sencillo de tales funtores es el funtor $1+(-):\mathbf{Con}\rightarrow\mathbf{Con}$, una de cuyas álgebras es $(\mathbb{N},[0,s]:1+\mathbb{N}\rightarrow\mathbb{N})$, donde $0:1\rightarrow\mathbb{N}$ es el cero y $s:\mathbb{N}\rightarrow\mathbb{N}$ la función sucesor.
     Otros funtores polinomiales importantes son aquellos en los que aparecen conjuntos constantes, como el funtor $1+A\times (-):\mathbf{Con}\rightarrow\mathbf{Con}$, una de cuyas álgebras es el álgebra de listas finitas sobre el conjunto $A$; o sea, $(A^\ast,[\mathrm{\textbf{nil}},\mathrm{\textbf{cons}}]:1+A\times A^\ast\rightarrow A^\ast)$, con $\mathrm{\textbf{nil}}:1\rightarrow A^\ast$ la lista vacía y $\mathrm{\textbf{cons}}:A\times A^\ast\rightarrow A$ la prefijación de un elemento de tipo $A$ a una lista; o como el funtor $1+X\times A\times X$, una de cuyas álgebras es el álgebra de árboles finitos binarios enraizados con nodos en $A$; o sea, $(\mathrm{\textbf{Árbol}}(A),[\mathrm{\textbf{nil}},\mathrm{\textbf{nodo}}]:1+\mathrm{\textbf{Árbol}}(A)\times A\times\mathrm{\textbf{Árbol}}(A)\rightarrow\mathrm{\textbf{Árbol}}(A))$, con $\mathrm{\textbf{nil}}:1\rightarrow\mathrm{\textbf{Árbol}}(A)$ el árbol binario enraizado vacío y $\mathrm{\textbf{nodo}}:\mathrm{\textbf{Árbol}}(A)\times A\times\mathrm{\textbf{Árbol}}(A)\rightarrow\mathrm{\textbf{Árbol}}(A)$ la construcción de un árbol binario enraizado a partir de dos (sub)árboles y una raíz en $A$.
     Pasemos a las coálgebras y veamos algunos ejemplos. Consideremos una máquina que es una caja negra y que tiene dos botones, $\mathrm{\textbf{val}}$ y $\mathrm{\textbf{sig}}$. Presionar el botón $\mathrm{\textbf{val}}$ resulta en alguna indicación visible del estado interno de la máquina, indicación cuyos valores están en el conjunto de datos $A$; tal operación no afecta el estado interno de la máquina, así que presionar dos veces $\mathrm{\textbf{val}}$ da el mismo resultado. Si uno presiona el botón $\mathrm{\textbf{sig}}$, la máquina cambia de estado, cuyo valor puede inspeccionarse al presionar nuevamente $\mathrm{\textbf{val}}$. Esta máquina puede describirse de manera abstracta como una coálgebra con mapeo de estructura $$(\mathrm{\textbf{val}},\mathrm{\textbf{sig}}):X\rightarrow A\times X,$$ donde $X$ es el espacio de estados (internos) de la máquina. Un coálgebra del funtor $A\times(-)$ es la coálgebra de listas infinitas sobre $A$; a saber, $(A^\mathbb{N},(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}}):A^\mathbb{N}\rightarrow A\times A^\mathbb{N})$, donde $\mathrm{\textbf{cab}}:A^\mathbb{N}\rightarrow A$ nos da el primer elemento de una lista infinita y $\mathrm{\textbf{cola}}:A^\mathbb{N}\rightarrow A^\mathbb{N}$ nos da la lista que resulta de quitar el primer elemento de la lista. Otra máquina caja negra podría ser una con un botón y una luz. La máquina realiza una acción sólo si el botón es presionado y la luz se enciende sólo si la máquina se detiene por completo; así que lo único que podríamos observar es su comportamiento tras presionar el botón y si se enciende la luz. Esta máquina puede describirse como una coálgebra con mapeo de estructura $$\mathrm{\textbf{botón}}:X\rightarrow 1+X,$$ donde $\mathrm{\textbf{botón}}\, s=\ast$ si la máquina deja de operar tras presionar el botón y se enciende la luz, y $\mathrm{\textbf{botón}}\,s\in X$ si la máquina no deja de operar y ha cambiado de estado. Una coálgebra del funtor $1+(-):\mathbf{Con}\rightarrow\mathbf{Con}$ es $(\overline{\mathbb{N}},\mathrm{\textbf{pred}}:\overline{\mathbb{N}}\rightarrow 1+\overline{\mathbb{N}})$, donde $\overline{\mathbb{N}}:=\mathbb{N}+\{\infty\}$ y $\mathrm{\textbf{pred}}(0):=\ast$, $\mathrm{\textbf{pred}}(n+1):=n$ y $\mathrm{\textbf{pred}}(\infty):=\infty$.
     Volvamos a las álgebras y expliquemos mediante el ejemplo de los números naturales la correspondencia entre inducción e inicialidad. La $1+(-)$-álgebra $(\mathbb{N},[0,s])$ es álgebra inicial en la categoría de álgebras del funtor $1+(-):\mathbf{Con}\rightarrow\mathbf{Con}$. En efecto, sean $A\in \mathbf{Con}$, $\varphi : \mathbb{N} \rightarrow A$ una función y $[d,r] : 1+A \rightarrow A$ una $1+(-)$-álgebra. Entonces, considérense los siguientes diagramas: $$\begin{xy} \xymatrix{ 1 \ar[d]_1 \ar[r] & 1+\mathbb{N} \ar[d]^{1+\varphi} & \mathbb{N} \ar[l] \ar[d]^{\varphi} & 1 \ar[r] \ar[rd]_0 & 1+\mathbb{N} \ar[d]^{[0,s]} & \mathbb{N} \ar[l] \ar[ld]^s \\ 1 \ar[r] \ar[rd]_d & 1+A \ar[d]^{[d,r]} & A \ar[l] \ar[ld]^r & & \mathbb{N} \ar[d]^{\varphi} & \\ & A & & & A & . }\end{xy}$$ De aquí, $$\begin{xy} \xymatrix{ 1+\mathbb{N} \ar[r]^{1+\varphi} \ar[d]_{[0,s]} \ar@{}[rd]|{=} & 1+A \ar[d]^{[d,r]} \ar@{}[rd]^(.6){\Leftrightarrow} & 1 \ar[r]^0 \ar@<-.5ex>[rd]_d \ar@<.5ex>@{}[rd]^{=} & \mathbb{N} \ar[r]^s \ar[d]^{\varphi} \ar@{}[rd]|{=} & \mathbb{N} \ar[d]^{\varphi} \\ \mathbb{N} \ar[r]_{\varphi} & A & & A \ar[r]_r & A; }\end{xy}$$ entonces, si $\varphi$ es un homomorfismo de álgebras, $\varphi$ tiene que cumplir que para todo $n\in \mathbb{N}$ $$\begin{xy} \xymatrix{ & 1 \ar[d]^0 \ar[ld]_d \\ A \ar[d]_{r^n} & \mathbb{N} \ar[l]_{\varphi} \ar[d]^{s^n} \\ A & \mathbb{N} \ar[l]^{\varphi} }\end{xy}$$ conmuta; por lo tanto, $\varphi n = r^n d$ para todo $n\in \mathbb{N}$.
     Luego, $(\mathbb{N},[0,s] : 1+\mathbb{N} \rightarrow \mathbb{N})$ es inicial.
     Observemos que pudimos haber obtenido el conjunto portador del álgebra inicial del funtor $1+(-)$ como el conjunto de los términos cerrados (los términos básicos —ground terms en inglés—, los que no tienen variables), es decir, de aquellos términos que son generados al aplicar iteradamente los constructores $\mathbf{0}:1\rightarrow X$ y $\mathbf{S}:X\rightarrow X$ de un álgebra cualquiera $(X,[\mathbf{0},\mathbf{S}]:1+X\rightarrow X)$ de $1+(-)$: $$\{\mathbf{0},\mathbf{S}\mathbf{0},\mathbf{S}\mathbf{S}\mathbf{0},\mathbf{S}\mathbf{S}\mathbf{S}\mathbf{0},\ldots\}.$$ En general, el conjunto portador del álgebra inicial de un funtor $T$ se puede obtener a partir de los términos cerrados, es decir, a partir de aquellos que son generados al aplicar iteradamente los constructores de un álgebra de $T$.
     Ahora el principio de inducción en los naturales usado como principio de demostración normalmente se formula de la siguiente manera: un subcojunto $P$ de $\mathbb{N}$ es igual a $\mathbb{N}$ si $0\in P$ y $n\in P\Rightarrow n+1\in P$. Reformulándolo, las suposiciones inductivas sobre $P$ esencialmente dicen que $P$ tiene una estructura de álgebra $0' : 1 \rightarrow P$, $s' : P \rightarrow P$ tal que la función inclusión $i : P \rightarrow \mathbb{N}$ es un homomorfismo de álgebras: $$\begin{xy} \xymatrix{ 1+P \ar[r]^{1+i} \ar[d]_{[0',s']} & 1+\mathbb{N} \ar[d]^{[0,s]} \\ P \ar[r]_i & \mathbb{N}. }\end{xy}$$ Es decir, $P$ es una subálgebra de $\mathbb{N}$. Ahora, de la inicialidad de $(\mathbb{N},[0,s])$, existe un homomorfismo $j : \mathbb{N} \rightarrow P$; nuevamente, por la inicialidad de $(\mathbb{N},[0,s])$, $i\circ j = 1_{\mathbb{N}}$: $$\begin{xy} \xymatrix{ 1+\mathbb{N} \ar[r]^{1+j} \ar[d]_{[0,s]} \ar@/^2pc/[rr]^{1+1_{\mathbb{N}}} & 1+P \ar[r]^{1+i} \ar[d]^{[0',s']} & 1+\mathbb{N} \ar[d]^{[0,s]} \\ \mathbb{N} \ar[r]_j \ar@/_2pc/[rr]_{1_{\mathbb{N}}} & P \ar[r]_i & \mathbb{N}; }\end{xy}$$ de aquí, $P = \mathbb{N}$.
     Veamos un ejemplo de cómo usar la inicialidad para las definiciones por inducción. Supongamos que queremos definir por inicialidad la función $fn=2^{-n}$ de los números naturales $\mathbb{N}$ a los racionales $\mathbb{Q}$. Las ecuaciones inductivas que la definen son $$f0:=1\qquad\text{y}\qquad f(n+1):=\frac{1}{2}fn.$$ Para definir esta función $f:\mathbb{N}\rightarrow\mathbb{Q}$ por inicialidad, hay que dotar a $\mathbb{Q}$ de una estructura de álgebra $1+\mathbb{Q}\rightarrow\mathbb{Q}$. Esta álgebra sobre $\mathbb{Q}$ corresponde al lado derecho de las dos ecuaciones inductivas que definen a $f$: $$\begin{xy} \xymatrix{ 1\ar[r]^1 & \mathbb{Q} & & \mathbb{Q}\ar[r]^{\frac{1}{2}(-)} & \mathbb{Q} }\end{xy}$$ $$\begin{xy} \xymatrix{ \ast\ar@{|->}[r] & 1 & & \ x\ar@{|->}[r] & \frac{1}{2}x. }\end{xy}$$ Entonces, $fn=2^{-n}$ está determinada por inicialidad como la única función que hace conmutar el siguiente diagrama: $$\begin{xy} \xymatrix{ 1+\mathbb{N}\ar[rr]^{1+f}\ar[d]_{[0,s]} & & 1+\mathbb{Q}\ar[d]^{[1,\frac{1}{2}(-)]}\\ \mathbb{N}\ar[rr]_f & & \mathbb{Q} }\end{xy}$$ La conmutatividad del diagrama nos da de vuelta las ecuaciones inductivas que definen a $f$. Notemos que los constructores $0$ y $s$ aparecen “dentro” de la función $f$, que estamos definiendo: $f0=1$ y $fsn=fn$.
     Esto muestra cómo se puede usar la inicialidad para definir funciones por inducción: hay que dotar al codominio de la función en cuestión de un estructura algebraica apropiada que corresponda a las cláusulas inductivas que determinan a dicha función. Además, en las definiciones inductivas, los constructores aparecen “dentro” de la función que se desea definir. Resumiendo: definir por inicialidad a una función es dotar a su codominio de una estructura algebraica apropiada que nos da la existencia de la función a definir, el diagrama conmutativo nos da las ecuaciones inductivas que determinan a la función; recíprocamente, las ecuaciones inductivas que definen a una función nos dan la estructura algebraica apropiada del codominio de la función para obtener su existencia mediante la inicialidad.
     Volvamos a las coálgebras y veamos la correspondencia entre terminalidad y coinducción. La coálgebra terminal (o final) del funtor $A\times(-):\mathbf{Con}\rightarrow\mathbf{Con}$ es $(A^\mathbb{N},(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}}))$, donde $\mathrm{\textbf{cab}}\,\sigma=\sigma\,0$ y $\mathrm{\textbf{cola}}\,\sigma=\lambda x.\sigma(x+1)$. En efecto, considérense los siguientes diagramas: $$\begin{xy} \xymatrix{ & X\ar[d]^{(\mathrm{\textbf{val}},\mathrm{\textbf{sig}})}\ar[dl]_{\mathrm{\textbf{val}}}\ar@/^0.9pc/[dr]^{\mathrm{\textbf{sig}}} & & & X\ar[d]^\varphi &\\ A\ar[d]_1 & A\times X\ar[r]\ar[l]\ar[d]^{A\times\varphi} & X\ar[d]^\varphi & & A^\mathbb{N}\ar[d]^{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})}\ar@/^1.3pc/[dr]^{\mathrm{\textbf{cola}}}\ar[dl]_{\mathrm{\textbf{cab}}} &\\ A & A\times A^\mathbb{N}\ar[r]\ar[l] & A^\mathbb{N} & A & A\times A^\mathbb{N}\ar[r]\ar[l] & A^\mathbb{N}. }\end{xy}$$ De aquí, $$\begin{xy} \xymatrix{ X \ar[r]^\varphi \ar[d]_{(\mathrm{\textbf{val}},\mathrm{\textbf{sig}})} \ar@{}[rd]|{=} & A^\mathbb{N} \ar[d]^{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})} \ar@{}[drr]^(.65){\Leftrightarrow} & & & X\ar@<-.5ex>[dl]_{\mathrm{\textbf{val}}}\ar@<.5ex>@{}[dl]^{=} \ar[d]^\varphi \ar@{}[rd]|{=} & X \ar[l]_{\mathrm{\textbf{sig}}}\ar[d]^\varphi \\ A\times X \ar[r]_{A\times\varphi} & A\times A^\mathbb{N} & & A & A^\mathbb{N}\ar[l]^{\mathrm{\textbf{cab}}} & A^\mathbb{N}\ar[l]^{\mathrm{\textbf{cola}}} }\end{xy}$$ entonces, si $\varphi$ es un homomorfismo de coálgebras, $\varphi$ tiene que cumplir que para todo $n\in \mathbb{N}$ $$\begin{xy} \xymatrix{ X \ar[r]^\varphi \ar[d]_{\mathrm{\textbf{sig}}^n} & A^\mathbb{N} \ar[d]^{\mathrm{\textbf{cola}}^n} \\ X \ar[r]_\varphi \ar[rd]_{\mathrm{\textbf{val}}} & A^\mathbb{N} \ar[d]^{\mathrm{\textbf{cab}}} \\ & A }\end{xy}$$ conmuta; por lo tanto, $\varphi(x)(n)=\mathrm{\textbf{val}}(\mathrm{\textbf{sig}}^nx)$ para todo $n\in\mathbb{N}$, ya que $\varphi(x)(n)=\mathrm{\textbf{cab}}(\mathrm{\textbf{cola}}^n\varphi x)$ para todo $n\in\mathbb{N}$.
     Luego, $(A^\mathbb{N},(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}}):A^\mathbb{N}\rightarrow A\times A^\mathbb{N})$ es terminal.
     Observemos que pudimos haber obtenido el conjunto portador de la coálgebra terminal del funtor $A\times(-)$ como el conjunto de todos los posibles comportamientos de un elemento $x\in X$, el conjunto de los comportamientos que se podría observar de $x$; es decir, podemos obtener el portador de la coálgebra del funtor $A\times(-)$ al aplicar iteradamente los observadores $\mathrm{\textbf{cab}}:X\rightarrow A$ y $\mathrm{\textbf{sig}}:X\rightarrow X$ a cualquier elemento $x$ de una coálgebra cualquiera $(X,(\mathrm{\textbf{val}},\mathrm{\textbf{sig}}):X\rightarrow A\times X)$ de $A\times(-)$: todas las posibles listas infinitas $$(\mathrm{\textbf{val}}\,x,\mathrm{\textbf{val}}(\mathrm{\textbf{sig}}\,x),\mathrm{\textbf{val}}(\mathrm{\textbf{sig}}^2\,x),\ldots).$$ En general, el conjunto portador de la coálgebra terminal de un funtor $T$ se puede obtener a partir de los comportamientos observables.
     La técnica para definir una función $f:X\rightarrow A$ por terminalidad es la siguiente: se describen las observaciones directas junto con las pasos siguientes solos de $f$ como una estructura coalgebraica sobre $X$. La función $f$ entonces surge por repetición. De aquí, una definición coinductiva de $f$ no determina a $f$ en una sola vez, sino pasa a paso. Veamos esto con unos ejemplos.
     Para nuestro funtor $A\times(-)$ sea $A=\mathbb{N}$. Definamos por coinducción la función $\mathrm{\textbf{desde}}:\mathbb{N}\rightarrow\mathbb{N}^\mathbb{N}$, la cual manda un número natural $n\in\mathbb{N}$ a la sucesión $(n,n+1,n+2,n+3,\ldots)\in\mathbb{N}^\mathbb{N}$. Esto implica definir una estructura coalgebraica $\mathbb{N}\rightarrow\mathbb{N}\times\mathbb{N}$ sobre $\mathbb{N}$. La observación directa que podemos hacer acerca del “estado” $n\in\mathbb{N}$ es $n$ mismo y el estado siguiente es $n+1$ (acerca del cual podemos observar directamente $n+1$). La repetición entonces nos lleva a $\mathrm{\textbf{desde}}\, n$. Definimos entonces por terminalidad a $\mathrm{\textbf{desde}}$ en el siguiente diagrama: $$\begin{xy} \xymatrix{ \mathbb{N}\ar[rr]^{\mathrm{\textbf{desde}}}\ar[d]_{\lambda n.(n,n+1)} & & \mathbb{N}^\mathbb{N}\ar[d]^{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})}\\ \mathbb{N}\times\mathbb{N}\ar[rr]_{1\times\mathrm{\textbf{desde}}} & & \mathbb{N}\times\mathbb{N}^\mathbb{N}. }\end{xy}$$ Así que $\mathrm{\textbf{desde}}$ queda determinada por las ecuaciones coinductivas $$\mathrm{\textbf{cab}}(\mathrm{\textbf{desde}}\, n)=n\quad\text{y}\quad\mathrm{\textbf{cola}}(\mathrm{\textbf{desde}}\, n)=\mathrm{\textbf{desde}}(n+1).$$      Definamos otras tres funciones, dos por coinducción. Nuevamente, consideremos el funtor $A\times(-)$. Definamos por terminalidad y, en consecuencia, por coinducción la función $\mathrm{\textbf{non}}:A^\mathbb{N}\rightarrow A^\mathbb{N}$ que, dada una lista infinita, devuelve la lista que resulta de tomar sólo los elementos en las entradas impares de la lista original; dotemos entonces a $A^\mathbb{N}$ de una estructura coalgebraica que nos dé las observaciones que queremos: $$\begin{xy} \xymatrix{ A^\mathbb{N}\ar[rr]^{\mathrm{\textbf{non}}}\ar[d]_{\lambda\sigma.(\mathrm{\textbf{cab}}\,\sigma,\mathrm{\textbf{cola}}(\mathrm{\textbf{cola}}\,\sigma))} & & A^\mathbb{N}\ar[d]^{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})}\\ A\times A^\mathbb{N}\ar[rr]_{1\times\mathrm{\textbf{non}}} & & A\times A^\mathbb{N} }\end{xy}$$ La estructura coalgebraica sobre $A^\mathbb{N}$ a la izquierda da lugar, por terminalidad, a un único homomorfismo de coálgebras. Por conmutatividad, $\mathrm{\textbf{non}}$ queda determinada por las ecuaciones coinductivas $$\mathrm{\textbf{cab}}(\mathrm{\textbf{non}}\,\sigma)=\mathrm{\textbf{cab}}\,\sigma\quad\text{y}\quad\mathrm{\textbf{cola}}(\mathrm{\textbf{non}}\,\sigma)=\mathrm{\textbf{non}}(\mathrm{\textbf{cola}}(\mathrm{\textbf{cola}}\,\sigma)).$$ Ahora, definimos $\mathrm{\textbf{par}}:=\mathrm{\textbf{non}}\circ\mathrm{\textbf{cola}}$, que es la función que, dada una lista infinita, nos devuelve una lista que resulta de tomar sólo los elementos en las entradas pares de la lista original.
     Finalmente, definamos por terminalidad y, en consecuencia, por coinducción la función $\mathrm{\textbf{fus}}:A^\mathbb{N}\times A^\mathbb{N}\rightarrow A^\mathbb{N}$ que, dada dos listas infinitas $\sigma$ y $\tau$, nos devuelve una lista que resulta de tomar elementos de $\sigma$ y $\tau$ alternadamente, empezando por $\sigma$; dotemos entonces a $A^\mathbb{N}\times A^\mathbb{N}$ de una estructura coalgebraica que nos dé las observaciones que queremos: $$\begin{xy} \xymatrix{ A^\mathbb{N}\times A^\mathbb{N}\ar[rr]^{\mathrm{\textbf{fus}}}\ar[d]_{\lambda(\sigma,\tau).(\mathrm{\textbf{cab}}\,\sigma,(\tau,\mathrm{\textbf{cola}}\,\sigma))} & & A^\mathbb{N}\ar[d]^{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})}\\ A\times(A^\mathbb{N}\times A^\mathbb{N})\ar[rr]_{1\times\mathrm{\textbf{fus}}} & & A\times A^\mathbb{N}. }\end{xy}$$ El homomorfismo $\mathrm{\textbf{fus}}:A^\mathbb{N}\times A^\mathbb{N}\rightarrow A^\mathbb{N}$ queda entonces determinado por las ecuaciones coinductivas $$\mathrm{\textbf{cab}}(\mathrm{\textbf{fus}}(\sigma,\tau))=\mathrm{\textbf{cab}}\,\sigma\quad\text{y}\quad\mathrm{\textbf{cola}}(\mathrm{\textbf{fus}}(\sigma,\tau))=\mathrm{\textbf{fus}}(\tau,\mathrm{\textbf{cola}}\,\sigma).$$      Lo que podemos ver de nuestras tres definiciones por coinducción es (1) que definir por terminalidad a una función es dotar a su dominio de una estructura coalgebraica apropiada que nos da la existencia de la función a definir, el diagrama conmutativo nos da las ecuaciones coinductivas que determinan a la función; recíprocamente, las ecuaciones coninductivas que definen a una función nos dan la estructura coalgebraica apropiada del dominio de la función para obtener su existencia mediante la terminalidad, y (2) que la función que queremos definir ocurre “dentro” de los observadores (o destructores) de la coálgebra terminal.
     En resumen, en una definición inductiva de una función $f$, uno define los valores de $f$ al hacerlo en todos los constructores de un álgebra inicial y en una definición coinducitva de $f$ uno define los valores de todos los observadores en cada resultado $fx$.
     Retomando la cóalgebra final del funtor $A\times(-)$ y los homomorfismos de coálgebras $\mathrm{\textbf{fus}},\mathrm{\textbf{non}}$ y $\mathrm{\textbf{par}}$, demostremos por coinducción que $$\mathrm{\textbf{fus}}(\mathrm{\textbf{non}}\,\sigma,\mathrm{\textbf{par}}\,\sigma)=\sigma;$$ es decir, hagamos uso de la unicidad dada por la terminalidad. Basta mostrar entonces que $\mathrm{\textbf{fus}}\circ(\mathrm{\textbf{non}},\mathrm{\textbf{par}}):A^\mathbb{N}\rightarrow A^\mathbb{N}$ es un homomorfismo de coálgebras $(A^\mathbb{N},(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}}))\rightarrow(A^\mathbb{N},(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}}))$; para esto, basta mostrar que $(\mathrm{\textbf{non}},\mathrm{\textbf{par}})$ es un homomorfismo de coálgebras. Notemos que la estructura coalgebraica sobre $A^\mathbb{N}\times A^\mathbb{N}$ la podemos reescribir como $(\mathrm{\textbf{cab}}\circ p_1,\mathrm{\textbf{int}})$, donde $p_1$ es la proyección izquierda de $A^\mathbb{N}\times A^\mathbb{N}$ e $\mathrm{\textbf{int}}(\sigma,\tau):=(\tau,\mathrm{\textbf{cola}}\,\sigma)$. El siguiente diagrama conmuta: $$\begin{xy} \xymatrix{ A^\mathbb{N}\ar[rr]^{(\mathrm{\textbf{non}},\mathrm{\textbf{par}})}\ar[d]_{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})} & & A^\mathbb{N}\times A^\mathbb{N}\ar[d]^{(\mathrm{\textbf{cab}}\circ p_1,\mathrm{\textbf{int}})}\\ A\times A^\mathbb{N}\ar[rr]_(.42){1\times(\mathrm{\textbf{non}},\mathrm{\textbf{par}})} & & A\times(A^\mathbb{N}\times A^\mathbb{N}), }\end{xy}$$ pues $\mathrm{\textbf{non}}\circ\mathrm{\textbf{cola}}=\mathrm{\textbf{par}}$ y $\mathrm{\textbf{cola}}\circ\mathrm{\textbf{non}}=\mathrm{\textbf{non}}\circ\mathrm{\textbf{cola}}\circ\mathrm{\textbf{cola}}$.
     El principio de coinducción como principio de demostración puede formularse de otra manera, mediante el concepto de bisimulación.
     Retomemos la coálgebra final del funtor $A\times(-)$. Una bisimulación sobre $A^\mathbb{N}$ es una relación $R$ sobre $A^\mathbb{N}$ tal que $$R(\sigma,\tau)\Rightarrow \begin{cases} \mathrm{\textbf{cab}}\,\sigma=\mathrm{\textbf{cab}}\,\tau\,\text{ y}\\ R(\mathrm{\textbf{cola}}\,\sigma,\mathrm{\textbf{cola}}\,\tau). \end{cases} $$ Ahora, $A^\mathbb{N}$ cumple el principio coinductivo de demostración: para todo $\sigma,\tau\in A^\mathbb{N}$, $$\text{si }R(\sigma,\tau)\text{ para alguna bisimulación }R\text{ sobre }A^\mathbb{N},\text{ entonces }\sigma=\tau.$$ Demostremos, otra vez, que $\mathrm{\textbf{fus}}(\mathrm{\textbf{non}}\,\sigma,\mathrm{\textbf{par}}\,\sigma)=\sigma$. Definamos la relación $$R:=\{(\mathrm{\textbf{fus}}(\mathrm{\textbf{non}}(\sigma),\mathrm{\textbf{par}}(\sigma)),\sigma)\mid\sigma\in A^\mathbb{N}\}$$ sobre $A^\mathbb{N}$. Se tiene que $R$ es una bisimulación, pues $$\mathrm{\textbf{cab}}(\mathrm{\textbf{fus}}(\mathrm{\textbf{non}}\,\sigma,\mathrm{\textbf{par}}\,\sigma))=\mathrm{\textbf{cab}}\,\sigma$$ y $$\mathrm{\textbf{cola}}(\mathrm{\textbf{fus}}(\mathrm{\textbf{non}}\,\sigma,\mathrm{\textbf{par}}\,\sigma))=\mathrm{\textbf{fus}}(\mathrm{\textbf{non}}(\mathrm{\textbf{cola}}\,\sigma),\mathrm{\textbf{par}}(\mathrm{\textbf{cola}}\,\sigma)),$$ y esto último nos dice que $R(\mathrm{\textbf{cola}}(\mathrm{\textbf{fus}}(\mathrm{\textbf{non}}\,\sigma,\mathrm{\textbf{par}}\,\sigma)),\mathrm{\textbf{cola}}\,\sigma)$, así que, por el principio coinductivo de demostración basado en una bisimulación, se obtiene la igualdad.
     El principio funciona por lo siguiente. Dado un funtor $T:\mathbf{Con}\rightarrow\mathbf{Con}$, una bisimulación sobre la $T$-coálgebra $(X,\chi)$ es una relación $R$ sobre $X$ para la que existe una estructura $T$-coalgebraica $\gamma:R\rightarrow TR$ tal que las proyecciones $\pi_1:R\rightarrow X$, $\pi_2:R\rightarrow X$ son homomorfismos de $T$-coálgebras. Si $(X,\chi)$ es la coálgebra final de la categoría de $T$-coálgebras, entonces $\pi_1=\pi_2$.
     En el caso anterior, una relación $R$ es una bisimulación si y sólo si el siguiente diagrama conmuta: $$\begin{xy} \xymatrix{ A^\mathbb{N}\ar[d]_{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})} & R\ar[r]^{\pi_2}\ar[l]_(.45){\pi_1}\ar[d]^{(\mathrm{\textbf{val}},\mathrm{\textbf{sig}})} & A^\mathbb{N}\ar[d]^{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})}\\ A\times A^\mathbb{N} & A\times R\ar[r]_{1\times\pi_2}\ar[l]^(.45){1\times\pi_1} & A\times A^\mathbb{N} }\end{xy}$$ si y sólo si $\mathrm{\textbf{cab}}\,\sigma=\mathrm{\textbf{val}}(\sigma,\tau)=\mathrm{\textbf{cab}}\,\tau$ con $\mathrm{\textbf{cola}}\,\sigma=\pi_1\,\mathrm{\textbf{sig}}(\sigma,\tau)$ y $\mathrm{\textbf{cola}}\,\tau=\pi_2\,\mathrm{\textbf{sig}}(\sigma,\tau)$, es decir, $R(\mathrm{\textbf{cola}}\,\sigma,\mathrm{\textbf{cola}}\,\tau)$.

Probando xyjax

Probemos unas flechas: \[ \begin{xy} \xymatrix{ a\ar[r]^f\ar[dr]^g & b\\ a & c } \end{xy} \] Y ahora otras: $$\begin{xy} \xymatrix{ 1+\mathbb{N} \ar[r]^{1+\varphi} \ar[d]_{[0,s]} \ar@{}[rd]|{=} & 1+A \ar[d]^{[d,r]} \ar@{}[rd]^(.6){\Leftrightarrow} & 1 \ar[r]^0 \ar@<-.5ex>[rd]_d \ar@<.5ex>@{}[rd]^{=} & \mathbb{N} \ar[r]^s \ar[d]^{\varphi} \ar@{}[rd]|{=} & \mathbb{N} \ar[d]^{\varphi} \\ \mathbb{N} \ar[r]_{\varphi} & A & & A \ar[r]_r & A }\end{xy}$$ Otra $$\begin{xy} \xymatrix{ x\ar@{}@<1.5ex>[d]_{=} & y\ar[d]_{\cong}\\ a & b }\end{xy}$$ Otra $$\begin{xy} \xymatrix{ x\rrtwocell & & y }\end{xy}$$