2 slightly expanded last para

I think the construction you're looking for can be seen as a right adjoint, and hence the details of the construction can be seen as coming from general transfinite constructions of adjoints.


Now, if I'm understanding right, the construction you're looking at, the "error-free core" of an $F+1$ coalgebra, is the right adjoint to this.

Moreover, I think there should be theorems that show automagically why this can be computed by the construction you give, as an $\omega$-long limit of pullbacks — but I'm not sure exactly where, I'm afraid. It's almost certainly deducible from the Kelly "Unified treatment of transfinite constructions" paper, well-described by Tom Leinster here; the constructions of that have a very similar flavour.

Relevant
