isMeasurable requires pointed type

[shinya-katsumata]

Hi, I am Shin-ya Katsumata at NII, invited to this project by Reynald.

I have a question: it appears that the measurable space whose carrier is the empty set (type) seems excluded from the definition, because isMeasurable requires a pointed type. I wonder why.

The standard definition of measurable space includes the empty one. Also, categorically, excluding the empty measurable space drastically changes the property of the category of measurable spaces.

[CohenCyril]

Dear Shin-ya Katsumata, you are completely right this definition alters the categorical properties of measurable spaces as types. This choice was made to have (partial) inverses for functions M -> T where M is a measurable type, indeed if M was not guaranteed to be non empty this would forbid having a generic inverse function.
On the other side, I believe types are not necessary the right pick for the carrier of objects in a category even in type theory, and that the empty measurable space could be represented by having an explicit "total set / domain predicate" field (in a distant future) so that by picking the empty set as the domain would add (infinitely many, albeit isomorphic, copies) of the empty measurable space...

[affeldt-aist]

NB: If one change pointed to choice in measure.v, all measure.v but one lemma and all measure_lebesgue.v go through.
lebesgue_integral.v fails at

analysis/theories/lebesgue_integral.v

Line 262 in f421377

Lemma mfun_subring_closed : subring_closed (@mfun _ aT rT).

where pointed it needed to have the structure of ring (1 != 0).

[CohenCyril]

Ha! This is really funny, because :1 != 0 also happens to be a anti-categorical oddity

[affeldt-aist]

Why does the 1 != 0 property belong to the mixin of rings?

[affeldt-aist]

Observation by @t6s : it should be easy to insert an intermediate mixin for non-necessarily not-trivial rings once MathComp 2.0 is available.

[CohenCyril]

Sorry I forgot to answer. Guillaume Cano added the intermediate structure in mathcomp 1, ten years ago, but it was never merged because of the huge impact it had on the library. Adding this structure is actually one of the reasons of existence of HB and mathcomp 2.