Is there such a thing as a weak coalgebra homomorphism?

Question

Given an endofunctor $F : Set \rightarrow Set$, we can define observation functions as functions that are polymorphic for any $F$-coalgebra, that is $obs$ is defined for any $F$-coalgebra $\langle A, c : A \rightarrow FA\rangle$. $$ obs : \forall \langle A, c \rangle . A \to B $$ Another way of looking at observation functions is as functions of the final $F$-coalgebra if it exists. We get the polymorphism automatically by composing the observation function with the unique homomorphism to the final $F$-coalgebra. But this only works if the final $F$-coalgebra exists.

One of the defining characteristics of an observation function is that it cancels any coalgebra homomorphism composed to the right, due to its polymorphism. If $hom$ is an $F$-coalgebra homomorphism, then: $$ obs = obs \circ hom $$ During my research, in an attempt to define a notion of observational consistency between one coalgebra and another, I had the idea of a weak coalgebra homomorphism. The idea is that we can "fake" a coalgebra homomorphism if we know the observation function ahead of time. Thus, we might satisfy, $$ obs = obs \circ hom $$ but only for one particular $obs$.

For example, let $FX = \{0,1\} \times X$, and let $obs$ be defined as $$ obs : \forall \langle A, c\rangle. A \to \{0,1\}^2 $$ $$ obs = \langle (\pi_1 \circ c), (\pi_1 \circ c \circ \pi_2 \circ c) \rangle $$ That is, $obs$ takes the first two elements of a stream.

Then, an F-coalgebra homomorphism would need to ensure that it preserves all the elements of the stream, whereas a weak homomorphism for $obs$ only needs to preserve the first two elements of the stream.

In my research, this notion would be useful in order to show that one coalgebra is observationally consistent with another by showing that every finite linear observation function has a weak homomorphism from the first coalgebra to the second coalgebra. In other words, every finite linear observation on the first coalgebra can be reproduced on the second coalgebra.

(What I mean by linear observation function feels mostly irrelevant, but for the sake of sharing... A linear observation function is more or less one that uses each state of the carrier set only once. I'm trying to model an oracle, and the user is not allowed to go back and pretend it never asked a question.)

My questions are thus:

1. Has this been researched? Do "weak coalgebra homomorphisms" exist already, under some other name perhaps?

2. Is there a more "category theory" way to present this?

Edit: Removed two questions which aren't that important.

Answer 1

The `weak morphisms' you describe do have a name in a slightly restricted setting. They can also be defined quite generally, as I'll explain.

In the case where $T : \mathsf{Set} \to \mathsf{Set}$ preserves weak pullbacks (many natural functors on $\mathsf{Set}$ do) it is known that behavioural equivalence coincides with coalgebraic bisimilarity. Then your morphisms are known as functional $\alpha$-step bisimulations where $\alpha$ is an ordinal. Admittedly I've only ever seen them defined for ordinals $\alpha \leq \omega$. Prior to coalgebra, modal logicians had studied n-step bisimulations for Kripke frames, which amount to n-step bisimulations for coalgebras for the powerset functor. Your requirement that they be functions as opposed to relations makes them functional n-step bisimulations.

On the other hand, you can define the concept you are talking about in a far more general setting without referring to coalgebraic bisimulations. For any category $\mathbb{C}$ which has limits of ordinal-indexed cochains and any functor $T : \mathbb{C} \to \mathbb{C}$ one can define $T$ 's terminal sequence. The condition regarding limits is actually rather weak e.g. many categories (including $\mathsf{Set}$) are actually complete i.e. have all small limits. The terminal sequence is a diagram in $\mathbb{C}$ and looks like:

$1 \quad \xleftarrow{!_{T1}} \quad T1 \quad \xleftarrow{T !_{T1}} \quad T^2 1 \quad \xleftarrow{T^2 !_{T1}} \quad \dots \quad T^\omega 1 \quad \xleftarrow{f_\omega^{\omega + 1}} \quad T(T^\omega 1) \quad \xleftarrow{Tf_\omega^{\omega + 1}} \quad \dots$

Here $1$ is the terminal object in $\mathbb{C}$ (limit of empty cochain). For example in $\mathsf{Set}$ this can be taken to be the one element set $1 = \{*\}$. The map $!_{T1} : T1 \to 1$ is the unique morphism into the terminal object e.g. in $\mathsf{Set}$ is simply maps every element of $T1$ to $*$. Each $T^n 1$ is computed by iterating $T$ and $T^\omega 1$ is the limit of the cochain preceding it. One can then continue beyond $\omega$, if necessary. Intuitively $T^\alpha 1$ is the collection of $\alpha$-step behaviours.

Now any $T$-coalgebra $(Z,\gamma)$ induces a cone over this sequence i.e. a collection of $\mathbb{C}$-morphisms $\mathsf{beh}_\gamma^\alpha : Z \to T^\alpha 1$ for each ordinal $\alpha$. I'll just define them for $\alpha < \omega$:

$\mathsf{beh}_\gamma^0 : Z \to 1$ is the unique map into the terminal object.

$\mathsf{beh}_\gamma^{n+1} = T\mathsf{beh}_\gamma^n \circ \gamma : Z \to T^{n+1} 1$

Intuitively these maps send a state in $Z$ to its $\alpha$-step behaviour. Now we can describe what you are talking about. Suppose we have two $T$-coalgebras $(A,\gamma)$ and $(B,\delta)$. Then a $\mathbb{C}$-morphism $f : A \to B$ preserves $\alpha$-step behaviour iff:

$\mathsf{beh}_\delta^\alpha \circ f = \mathsf{beh}_\gamma^\alpha$

That is, the $\alpha$-step behaviour of $f(z)$ in $\delta$ is precisely the $\alpha$-step behaviour of $z$ in $\gamma$.

Anyway, I hope this is helpful. You can find various references by googling 'terminal sequence coalgebra' or 'final sequence coalgebra'.

Answer 2

As a rule, one should avoid heavily overloaded terminology like weak, regular, normal, etc. unless the notion has some universality. In particular, it appears your notion doesn't correspond with the usual notion of weak homomorphism after arrow flipping.

There are always more descriptive terms whenever your doing something less universal, like "observationally weakened homomorphism" shortened to "ow-homomorphism" perhaps.

Your notion of observation function already provides a category theoretic presentation. I'd worry more about clarifying what exactly it means, and why it's interesting, rather than seeking the most generality possible. In particular, you should usually give an informative example and non-example when introducing unusual notions in print.