Came to the conclusion that the difference between Markov categories and Simpson's atomic sheaf framework (as illustrated on FinInj/FinSur) can be reduced to the difference between geometric and topological descriptions. The former track probability as a measure, while the latter tracks a more abstract independence structure. That is, if we want a synthetic type theory for probability/statistics, it makes sense to start by formalizing Simpson's framework in homotopy type theory.