Here is a list of various notions of probability measures developed in category theory, might be useful (with lots of references). I have no idea if any of these notions somehow fit well with linear logic though. That being said if you are aiming to create a language for bayesian probabilities, I think it would be interesting to look in particular into continuous valuations on dcpos (see previous link), and try to somehow apply this stuff to the framework developed by Paul Taylor , which gives a constructive account of topology. Plus he's quite opinionated and fun to read too.
And an aside on reflectivity. In general any sufficiently general logical construct does not have this property: set universes are not reflective; types of types in type theories are not either; NF is the one exception I know of but suffers from some pathologies such as not allowing currying. So overall I do not think this is a reasonable expectation to have. However toposes are partially reflective: their (impoverished) internal version of themselves is their set of truth values. A way to see this is that you get back the poset of truth values if you collapse all hom-sets of your topos into singletons (which is like seing all objects as propositions instead of sets). This is related to Lawvere-Tierney topologies , which give a way of "modifying" your topos through an operation on its set of truth values only (and this is equivalent to taking sheaves on a site in a presheaf topos, so pretty much all "nice" toposes arise in this way). I would use this as a guideline for what to expect of a reflective operation in a good enough probabilistic universe.
That being said if you are aiming to create a language for bayesian probabilities, I think it would be interesting to look in particular into continuous valuations on dcpos (see previous link), and try to somehow apply this stuff to the framework developed by Paul Taylor , which gives a constructive account of topology. Plus he's quite opinionated and fun to read too.
However toposes are partially reflective: their (impoverished) internal version of themselves is their set of truth values. A way to see this is that you get back the poset of truth values if you collapse all hom-sets of your topos into singletons (which is like seing all objects as propositions instead of sets).
This is related to Lawvere-Tierney topologies , which give a way of "modifying" your topos through an operation on its set of truth values only (and this is equivalent to taking sheaves on a site in a presheaf topos, so pretty much all "nice" toposes arise in this way).
I would use this as a guideline for what to expect of a reflective operation in a good enough probabilistic universe.