This interprets the P(AxX) functor in MDPs slightly differently.
Instead of using labels for choices, we use unlabeled transitions and
partition the choice-states on their choice instead in the initial
partition. This corresponds more faithfully to the graph
representation of the coalgebra in our program.