Commit 2026-03-27 14:36 a4f0758b

feat(Kernel/Category): Stoch is a Markov category (#36779)

• Define SFinKer, the category of measurable spaces and s-finite kernels. Show that it is a copy-discard category.

• Define Stoch, the category of measurable spaces and Markov kernels as a WideSubcategory of SFinKer. Show that it is a Markov category. It uses new typeclasses for MorphismProperty that are stables under specific morphisms of the original category.

• Add some useful lemmas about parallel product of kernels.