zig-zag is a span as well.

-   The functor $[0,1] \times (-)^A$ on  is proper, again the zig-zag being a span.

-   The functor ${{\ensuremath{\widehat F}}}$ on ${{\text{\tt{PCA}}}}$ is proper. This proof is the most involved, and interestingly, provides the only case where the zig-zag is not a span: it contains three intermediate nodes of which the middle one forms a span.

Our framework requires a proof of so-called *extension* and *reduction lemmas* in each case. While the extension lemma is a generic result that covers all cubic functors of interest, the reduction lemma is in all cases a nontrivial property intrinsic to the algebras under consideration. For the semiring of natural numbers it is a consequence of a result that we trace back to Hilbert; for the case of convex algebra $[0,1]$ the result is due to Minkowski. In the case of ${{\ensuremath{\widehat F}}}$, we use Kakutani’s set-valued fixpoint theorem.

It is an interesting question for future work whether these new properness results may lead to new complete axiomatizations of expressions for certain weighted automata.

The organization of the rest of the paper is as follows. In Section \[sec-ProperFunctors\] we give some basic definitions and introduce the semirings, the 