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".

A sheaf theoretic approach to measure theory, which gives another approach to developing measure theory in toposes. $\endgroup$ – Peter LeFanu Lumsdaine Jun 28 '17 at 10:17