${{\ensuremath{\widehat F}}}f=({{\ensuremath{F_{\,{[0,1]}}}}}f)|_{{{\ensuremath{\widehat F}}}X}$ for $f\colon X\to Y$.

Cubic functors are liftings of ${{\text{\tt{Set}}}}$-endofunctors, in particular, they preserve surjective algebra homomorphisms. It is easy to see that also the functor ${{\ensuremath{\widehat F}}}$ preserves surjectivity, cf. Lemma \[GhSurj\] (Appendix \[app:D\]) This property is needed to apply the work of Milius, cf. [@milius:2017 Assumptions 3.1].

\[ProperSemiring\] We can now formulate precisely the connection between proper semirings and proper functors mentioned after Definition \[Proper\]. A semiring $\mathbb S$ is proper in the sense of [@esik.maletti:2010], if and only if for every finite input alphabet $A$ the cubic functor ${{\ensuremath{F_{\,{\mathbb S}}}}}$ on ${\text{$\mathbb S$-{\text{\tt{SMOD}}}}}$ is proper.

We shall interchangeably think of direct products as sets of functions or as sets of tuples. Taking the viewpoint of tuples, the definition of ${{\ensuremath{F_{\,{\mathbb S}}}}}f$ reads as $$({{\ensuremath{F_{\,{\mathbb S}}}}}f)\big((o,(x_a)_{a\in A})\big)=\big(o,(f(x_a))_{a\in A}\big),\quad 
    o\in\mathbb S,\ x_a\in X\text{ for }a\in A
    .$$ A coalgebra structure $c\colon X\to{{\ensuremath{F_{\,{\mathbb S}}}}}X$ writes as $$c(x)=\big({{c}_{\text{\rm o}}}(x),({{c}_{a}}(x))_{a\in A}\big),\quad x\in X
    ,$$ and we use ${{c}_{\text{\rm o}}}:X\to\mathbb S$ and ${{c}_{a}}:X\to X$ as generic notation for the components of the map $c$. More generally, we define $c_w\colon X\to X$ for any word $w\in A^*$ inductively as ${{c}_{\varepsilon}}=\operatorname{id}_X$ and ${{c}_{wa}}={{c}_{a}}\circ{{c}_{w}},\ w\in A^*,a\in A$.

The map from a coalgebra $(X,c)$ 