algebraic categories and deterministic weighted automata functors on them. Such categories are the target of generalized determinization [@silva.bonchi.bonsangue.rutten:2010; @silva.sokolova:2011; @jacobs.silva.sokolova:2015] and enable coalgebraic modelling beyond sets. For example, non-deterministic automata, weighted, or probabilistic ones are coalgebraically modelled over the categories of join-semilattices, semimodules for a semiring, and convex sets, respectively. Moreover, expressions for axiomatizing behavior semantics often live in algebraic categories.

In order to prove completeness of such axiomatizations, the common approach [@silva:2010; @bonsangue.milius.silva:2011; @silva.sokolova:2011] is to prove finality of a certain object in a category of coalgebras over an algebraic category. Proofs are significantly simplified if it suffices to verify finality only w.r.t. coalgebras carried by free finitely generated algebras, as those are the coalgebras that result from generalized determinization.

In recent work, Milius [@milius:2017] proposed the notion of a proper functor on an algebraic category that provides a sufficient condition for this purpose. This notion is an extension of the notion of a proper semiring introduced by Esik and Maletti [@esik.maletti:2010]: A semiring is proper if and only if its “cubic" functor is proper. A cubic functor is a functor $\mathbb S \times (-)^A$ where $A$ is a finite alphabet and $\mathbb S$ is a free algebra with 