Suppose $F, T : Set \rightarrow Set$ are two functors on the category of sets. Let $F^{coalg}$, $T^{coalg}$ denote the categories of $F$, respectively $T$ coalgebras. Vaguely, I'm interested in when I can find a functor $G : F^{coalg} \rightarrow T^{coalg}$ that preserves my intuition from the final coalgebras of each functor.
Motivating example:
$F(-) = A \times -$
$T(-) = \mathcal{P}_{fin}(A \times -)$
Then $F$ has a final coalgebra of streams over $A$ (i.e. $F$ has fixed point of $A^{\mathbb{N}}$), and $T$ has a final coalgebra of equivalence classes of $A$-labeled transition systems with finite branching.
Now, my intuition says that I can map a stream over $A$ into a labeled transition system which has a path (i.e. a subtransition system with no branching) that has the same sequence of labels as my stream. But is there a way to formalize this mapping of streams into labeled transition systems via a functor $G$? I see two potential problems trying to do so:
(1) Streams and (equivalence classes of) labeled transition systems are the final coalgebras so although I described an intuitive map from streams to LTS's, I'm not sure what this map would like like for all the nonfinal coalgebras in $F^{coalg}$.
(2) I want to suggest something like G being a natural transformation from the identity functor to $\mathcal{P}_{fin}$, but I'm not quite sure what to do with the object or structure maps and am also not quite sure how to think about the nonfinal coalgebras.
Thanks!
Let $\eta : F \Rightarrow G$ be a natural transformation between functors $F, G : \mathbf C \to \mathbf C$. Then there is a functor $H : F\text{-}\mathbf{coalg} \to G\text{-}\mathbf{coalg}$. On objects, $H(A \xrightarrow{a} F(A)) = A \xrightarrow{a} F(A) \xrightarrow{\eta_A} G(A)$, and $H$ is the identity on morphisms, which gives $G$-colgebra homomorphisms by naturality of $\eta$.
For your example, note that $\mathcal P_f$ is a monad, and so there is a natural transformation $\mathrm{Id}_{\mathbf{Set}} \Rightarrow \mathcal P_f$. We can then left-whisker with the functor $A \times (-) : \mathbf{Set} \to \mathbf{Set}$ to get a natural transformation from $A \times (-) \Rightarrow \mathcal P_f(A \times -)$, which induces a functor $(A \times -)\text{-}\mathbf{coalg} \to P_f(A \times -)\text{-}\mathbf{coalg}$.