Terminology for this notion of "$\sigma$-algebra" in a topos

Question

Let $\mathcal{E}$ be a Grothendieck topos. I want to define a sort of "$\sigma$-algebra" for it, and I'm asking about what it should be—or already is—called. I know from nlab that Cheng spaces are an accepted constructive notion of $\sigma$-algebras but I don't yet see why I might find them interesting. So one may answer this question by instead telling me why my notion (see below) may not be well-behaved, or what's so nice about Cheng spaces. But let's leave that question aside for now.

In the proposed definition below, I'll use the internal language of $\mathcal{E}$. I'll use the convention that $A\Rightarrow B\Rightarrow C$ means $A\Rightarrow(B\Rightarrow C)$. I'll use $\lambda$ notation for terms of exponential objects; for example given types $X$ and $P$ and a term $p:P$, I'll write $\lambda(x:X)\ldotp p$ to denote the function $X\to P$ that is constant at $p$.

Definition: Let $\mathcal{E}$ be a Grothendieck topos, $\top\colon 1\to\Omega$ its subobject classifier, and $\mathbb{N}$ its natural numbers object. A pseudo-$\sigma$ algebra in $\mathcal{E}$ consists of an object $X$ and a morphism $\Sigma\colon \Omega^X\to\Omega$ satisfying the following axioms:

• $\forall(\omega:\Omega)\ldotp\Sigma\big(\lambda(x:X)\ldotp\omega\big)\;\;\;\;$ ["constant propositions are measurable"]
• $\forall(\phi,\psi:X\to\Omega)\ldotp \Sigma(\phi)\Rightarrow\Sigma(\psi)\Rightarrow\Sigma(\phi\wedge\psi)\;\;\;\;$ ["closed under $\wedge$"]
• $\forall(\phi,\psi:X\to\Omega)\ldotp \Sigma(\phi)\Rightarrow\Sigma(\psi)\Rightarrow\Sigma(\phi\vee\psi)\;\;\;\;$ ["closed under $\vee$"]
• $\forall(\phi,\psi:X\to\Omega)\ldotp \Sigma(\phi)\Rightarrow\Sigma(\psi)\Rightarrow\Sigma(\phi\Rightarrow\psi)\;\;\;\;$ ["closed under $\Rightarrow$"]
• $\forall(\phi:\mathbb{N}\to\Omega^X)\ldotp\big(\forall(n:\mathbb{N})\ldotp\Sigma(\phi(n))\big)\Rightarrow\Sigma\big(\forall(n:\mathbb{N})\ldotp\phi(n)\big)\;\;\;\;$ ["closed under countable $\forall$"]
• $\forall(\phi:\mathbb{N}\to\Omega^X)\ldotp\big(\forall(n:\mathbb{N})\ldotp\Sigma(\phi(n))\big)\Rightarrow\Sigma\big(\exists(n:\mathbb{N})\ldotp\phi(n)\big)\;\;\;\;$ ["closed under countable $\exists$"]

For any $\phi:X\to\Omega$, say that $\phi$ is measurable if $\Sigma(\phi)=\top$.

Question: What might be a more common, more useful, or better terminology for what I've called pseudo-$\sigma$ algebras?

I guess it's different than just a sub-Heyting algebra of $\Omega^X$ because of the "countable quantification".

Answer 1

This is an answer to the new question formulated in the comments.

Point-set notions of topological spaces are a poor fit for arbitrary toposes because constructing points typically requires the axiom of choice, whereas constructing the lattice of open sets does not. This is the reason why locales are used instead of topological spaces in this context.

This can be concisely illustrated by the following fact: in the presence of the axiom of choice, locally compact locales as well as compact regular locales are spatial, i.e., come from topological spaces.

For example, open sets in the Zariski spectrum of a commutative ring are radical ideals, whereas points are prime ideals, and proving that a ring has sufficiently many prime ideals requires the axiom of choice, whereas proving that it has sufficiently many radical ideals does not. Similar statements can be made about C*-algebras and other types of rings.

The situation for measure spaces is similar. First, if one looks at typical theorems in measure theory, it becomes clear that the data of a σ-algebra alone is never sufficient to formulate an interesting theorem in measure theory; one needs to know at least what the sets of measure 0 are (for more details, see Is there an introduction to probability theory from a structuralist/categorical perspective?).

If we adopt this new notion of measurable space (i.e., a set X, a σ-algebra M of measurable subsets, and a σ-ideal N of negligible sets, equivalently, a measure class), the resulting category of measurable spaces is equivalent to the category of measurable locales (see https://ncatlab.org/nlab/show/measurable+locale): given a measurable space (X,M,N), send it to the poset (a frame, in fact) M/N, i.e., equivalence classes of measurable sets modulo negligible sets.

One can then illustrate the above points (pun intended) for measurable spaces by considering the equivalence between commutative von Neumann algebras, measurable locales, and measurable spaces. A measurable locale can be extracted from a von Neumann algebra in a canonical fashion: it is simply the complete Boolean algebra of its projections. To extract a measurable space, however, one needs the axiom of choice: the points of the measurable space are maximal C*-ideals in the von Neumann algebra.

One must mention that measure theory in a topos has not yet been developed to the same extent that general topology is. For instance, the equivalence between commutative C*-algebras and compact regular locales is proven in a very satisfactory form in arXiv:1411.0898v1. There is no similar exposition for commutative von Neumann algebras and measurable locales in the literature. (I had some correspondence with Simon Henry about this, and the conclusion was that it seems like it can be done, but no details can be found in the literature.)