Nice! One itch: in the slides, \$$\text{FinStoch}\$$ has as objects just finite sets, while in \$$\text{FinProb}\$$ the objects are pairs of finite sets and distributions (and maps are measure preserving functions). Where does \$$f : (X,u_X) \to (Y,p) \$$ live?