This context of this question is Rutten's [Universal Coalgebra](http://en.wikipedia.org/wiki/F-coalgebra), used for modelling systems. I'm interested in finding a description of a functor between different types of coalgebras corresponding to finding a certain subcoalgebra.


An $F+1$-coalgebra $\langle S,\alpha:S\to F(S)+1\rangle$ can be thought of as a system whose transition shape is given by functor F plus the possibility of an error/termination, given by the +1. Assume that $F$ is a so-called Kripke polynomial functor: $F::=Id ~|~ B ~|~ F+F ~|~ F\times F ~|~ F^ A ~|~ \mathcal{P}\_\omega F$, thus it preserves pullbacks.


A subcoalgebra of $\langle S,\alpha:S\to F(S)+1\rangle$ is coalgebra $\langle S',\alpha':S'\to F(S')+1\rangle$, where $S'\subseteq S$ and $\alpha'$ is $\alpha'$ restricted to $S'$, such that its range falls within $F(S')+1$.


I want to find the maximal subcoalgebra of this coalgebra which corresponds to an $F$-coalgebra. In terms of my application, this means I'm looking for the subset of states $S'\subseteq S$ that do not lead to the error state.


Clearly, I can take the pullback of the functions $\alpha:S\to F(S)+1$ and $inl:F(S)\to F(S)+1$ to get a set $S\_0\subseteq S$ which do not lead to an error in the first step. Iterating this process for functors $F^i+1$ seems to lead to progressively smaller subsets $S\_i$ of $S$ each avoiding the error state for $i$ steps. What I'm lacking is a coherent description of the process.


Is whether there is a more universal description of this construction in terms of limits or colimits, or at least, some known approaches to the problem?


I asked this question on the computer science theory overflow ([here](https://cstheory.stackexchange.com/questions/901/maximal-subcoalgebras-of-an-f1-coalgebra-corresponding-to-an-f-coalgebra)), but am re-asking it here as I received no feedback.



Maximal subcoalgebras of an $F+1$-coalgebra corresponding to an $F$-coalgebra
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](https://mathoverflow.net/questions/19906/are-monads-monadic/20345#20345); the constructions of that have a very similar flavour.


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


