into the final ${{\ensuremath{F_{\,{\mathbb S}}}}}$-coalgebra, the *trace map*, is then given as $\operatorname{tr}_c(x)=\big(({{c}_{\text{\rm o}}}\circ{{c}_{w}})(x)\big)_{w\in A^*}$ for $ x\in X$. Behavioural equivalence for cubic functors is the kernel of the trace map.

Properness of cubic functors {#sec-PropernessCubic}
============================

Our proofs of properness in this section and in Section \[sec-PropernessSubcubic\] below start from the following idea. Let $\mathbb S$ be a semiring, and assume we are given two ${{\ensuremath{F_{\,{\mathbb S}}}}}$-coalgebras which have free finitely generated carrier, say $(\mathbb S^{n_1},c_1)$ and $(\mathbb S^{n_2},c_2)$. Moreover, assume $x_1\in\mathbb S^{n_1}$ and $x_2\in\mathbb S^{n_2}$ are two elements having the same trace. For $j=1,2$, let $d_j\colon \mathbb S^{n_1}\times\mathbb S^{n_2}  \to  {{\ensuremath{F_{\,{\mathbb S}}}}}(\mathbb S^{n_1}\times\mathbb S^{n_2})$ be given by $$d_j(y_1, y_2) = \Big({{c_j}_{\text{\rm o}}}(y_j),(({{c_1}_{a}}(y_1),{{c_2}_{a}}(y_2)))_{a\in A}\Big).$$ Denoting by $\pi_j\colon \mathbb S^{n_1}\times\mathbb S^{n_2}\to\mathbb S^{n_j}$ the canonical projections, both sides of the following diagram separately commute. $$\xymatrix@C=15pt@R=10pt@M=7pt{
    \mathbb S^{n_1} \ar[dd]_{c_1}
    && \mathbb S^{n_1}\times\mathbb S^{n_2} \ar[ll]_{\pi_1} \ar[rr]^{\pi_2} 
        \ar@/_15pt/[dd]_{d_1} \ar@/^15pt/[dd]^{d_2} 
    && \mathbb S^{n_2} \ar[dd]_{c_2}
    \\
    && \neq &&
    \\
    {{\ensuremath{F_{\,{\mathbb S}}}}}\mathbb S^{n_1} 
    && {{\ensuremath{F_{\,{\mathbb S}}}}}(\mathbb S^{n_1}\times\mathbb S^{n_2}) \ar[ll]_{{{\ensuremath{F_{\,{\mathbb S}}}}}\pi_1} \ar[rr]^{{{\ensuremath{F_{\,{\mathbb S}}}}}\pi_2}
    && {{\ensuremath{F_{\,{\mathbb S}}}}}\mathbb S^{n_2}
}$$ However, in general the maps $d_1$ and $d_2$ do not coincide.

The next lemma contains a simple observation: there exists a subsemimodule $Z$ of $\mathbb S^{n_1}\times\mathbb S^{n_2}$, such that 