a single generator in the algebraic category. Cubic functors model deterministic weighted automata which are models of determinizations of non-deterministic and probabilistic transition systems.

Properness is the property that for any two states that are behaviourally equivalent in coalgebras with free finitely generated carriers, there is a zig-zag of homomorphisms (called a chain of simulations in the original works on weighted automata and proper semirings) that identifies the two states and whose nodes are all carried by free finitely generated algebras.

Even though the notion of properness is relatively new for a semiring and very new for a functor, results on properness of semirings can be found in more distant literature as well. Here is a brief history, to the best of our knowledge:

-   The Boolean semiring was proven to be proper in [@bloom.esik:1993].

-   Finite commutative ordered semirings were proven to be proper in  [@esik.kuich:2001 Theorem 5.1]. Interestingly, the proof provides a zig-zag with at most seven intermediate nodes.

-   Any euclidean domain and any skew field were proven proper in [@beal.lombardy.sakarovitch:2005 Theorem 3]. In each case the zig-zag has two intermediate nodes.

-   The semiring of natural numbers $\mathbb N$, the Boolean semiring $\mathbb B$, the ring 