## Return to Answer

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.

$\newcommand{\inl}{\mathrm{inl}} \newcommand{\Coalg}{\mathbf{Coalg}}$ There's a functor $\inl^* : F$-$\Coalg \longrightarrow (F+1)$-$\Coalg$; it embeds $F$-coalgebras asthe full subcategory of "error-free" $F+1$-coalgebras, and is induced by the natural transformation $\inl : F \rightarrow F+1$ in an obvious-once-you-write-down-the-diagram way.

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

Possibly relevant well-known constructions to compare (in Kelly and elsewhere): the construction of an algebraically-(co)free (co)monad on an endofunctor, and ; the construction of the free $T$-algebra on a $T$-graph.T$-graph; the free$S$-algebra on a$T$-algebra, given a monad map$S \to T\$.

1

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.

$\newcommand{\inl}{\mathrm{inl}} \newcommand{\Coalg}{\mathbf{Coalg}}$ There's a functor $\inl^* : F$-$\Coalg \longrightarrow (F+1)$-$\Coalg$; it embeds $F$-coalgebras asthe full subcategory of "error-free" $F+1$-coalgebras, and is induced by the natural transformation $\inl : F \rightarrow F+1$ in an obvious-once-you-write-down-the-diagram way.

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 well-known constructions to compare (in Kelly and elsewhere): the construction of an algebraically-(co)free (co)monad on an endofunctor, and the construction of the free $T$-algebra on a $T$-graph.
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 25, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.920470654964447, "perplexity_flag": "middle"}