categories, and the functors of interest. Section \[sec-PropernessCubic\] provides the general framework as well as proofs of properness of the cubic functors. Section \[sec-SubcubicFunctor\]–Section \[sec-PropernessSubcubic\] lead us to properness of ${{\ensuremath{\widehat F}}}$ on . For space reasons, we present the ideas of proofs and constructions in the main paper and defer all detailed proofs to the appendix.

#### Acknowledgements.

We thank the anonymous reviewers for many valuable comments, in particular for reminding us of a categorical property that shortened the proof of the extension lemma (the proofs of Lemma \[lem:ext-lem-1\] and Lemma \[lem:ext-lem-2\] in Appendix \[app:B\]).

Proper functors {#sec-ProperFunctors}
===============

We start with a brief introduction of the basic notions from algebra and coalgebra needed in the rest of the paper, as well as the important definition of proper functors [@milius:2017]. We refer the interested reader to [@Rut00:tcs; @JR96:eatcs; @jacobs:2017] for more details. We assume basic knowledge of category theory, see e.g. [@maclane:1998] or Appendix \[sec:app-basics\].

Let ${\text{\tt{C}}}$ be a category and $F$ a ${\text{\tt{C}}}$-endofunctor. The category ${{\sf Coalg}({F})}$ of *$F$-coalgebras* is the category having as objects pairs $(X,c)$ where $X$ is an object of ${\text{\tt{C}}}$ and $c$ is a ${\text{\tt{C}}}$-morphism from $X$ to $FX$, and as morphisms $f\colon(X,c)\to(Y,d)$ those 