Free extension of nested partial unary operations ($F_n⊣G_n$)

For an object of the nested partial unary operation category ${\mathcal{C}}_n$, adjoining the next operation freely gives one new value at each defined fixed point of the previous operation. Each new value starts an infinite free chain under the first unary operation; the other old operations are undefined on those new points. The new top operation consequently has no fixed points, so subsequent free extensions add no points. This gives a left adjoint to forgetting the last operation; extensions of maps along the chains are forced by the first target operation.

In the nested partial unary operation category, suppose the lower-operation diagram $A\rightrightarrows B\stackrel{q}{\to }Q$ has a split coequalizer with $qs=1$, $ft=1$ and $gt=sq$. The section $s$ takes eligible fixed points to eligible fixed points, so the displayed next operation is defined on exactly the required domain. For eligible $x\in B$, the equations giveThus $q$ preserves the next operation. Every factored morphism preserves it by evaluating at $sz$, giving creation of the specified coequalizer. Together with reflection of isomorphisms, the Beck monadicity theorem proves one-step monadicity.