Split-coequalizer lifting for a fixed-point-domain operation (${\beta }_Q(z)=q{\beta }_B(sz)$)

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.