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.