A more involved, graphical, proof of this proposition may be found in [@D08] (Sections 6-8).

If our free adjunction is generated by a single object on the $\cal  A$ side, then we establish the isomorphism of $\cal  A$ with the category of the comonad freely generated by a single object (see the end of Section 2).

Bijunctions and self-adjunctions
================================

We call *trijunction* a structure made of the categories $\cal A$ and $\cal B$, the functor $U$ from $\cal A$ to $\cal B$, and the functors $L$ and $R$ from $\cal B$ to $\cal A$, such that $L$ is left adjoint to $U$, with the unit $\gamma^{\cal
B}\!:I_{\cal B}\strt UL$ and counit $\varphi^{\cal A}\!:LU\strt
I_{\cal A}$, and $R$ is right adjoint to $U$, with the unit $\gamma^{\cal A}\!:I_{\cal A}\strt RU$ and counit $\varphi^{\cal
B}\!:UR\strt I_{\cal B}$. This notion plays an important role in [@DP08b].

We call *bijunction* a trijunction where the functors $L$ and $R$ are equal. We write in this context $P$ instead of $L$ and $R$. (Various terms have been used for bijunctions and related notions: in [@M65] one finds *strongly adjoint* pairs of functors, in [@CMS97] *Frobenius functors*, in [@K02] *biadjunction*, which has already been introduced for 