A terminal coalgebra of a certain functor on Mes

Question

Let $\mathfrak C = \mathsf{Mes}$ be the category of meausurable spaces and measurable maps. For any object $X\in \mathfrak C_0$ we assign a measurable space $\mathcal P(X)$ whose elements $\mu$ are probability measures over $X$. The space $\mathcal P(X)$ is endowed with the smallest $\sigma$-algebra that makes evaluation maps $\mu\mapsto \mu(B)$ measurable.

Let further $A\in \mathfrak C_0$ be some fixed finite measurable space with a discrete $\sigma$-algebra and define an endofunctor $F$ on $\mathfrak C$ by

1. $F(X) = A\times \mathcal P(X)$ for any object $X\in \mathfrak C_0$

2. $F(f)(a,\mu) = (a,\mu\circ f^{-1})$ for any arrow $f\in \mathfrak C_1$, where $\mu\circ f^{-1}$ is the image measure.

I wonder if $F$ admits for a terminal coalgebra, and which shape does it have. I am as well interested whether $F$-coalgebras have been studies somewhere for $F$ as above.

Answer 1

Final coalgebras for functors on measurable spaces, Lawrence S. Moss and Ignacio D. Viglizzo:

"We prove that every functor on the category Meas of measurable spaces built from the identity and constant functors using products, coproducts, and the probability measure functor Δ has a final coalgebra."