Add the effective topos by dschepler · Pull Request #362 · ScriptRaccoon/CatDat

dschepler · 2026-09-08T22:05:10Z

Addresses #353

Currently unresolved properties:
is accessible
is coaccessible
has a cogenerating set
has a cogenerator
is concretizable
has an extremal cogenerating set
has an extremal cogenerator
has an extremal generating set
has an extremal generator
has a generating set
has a generator
is ℵ₁-accessible
has ℵ₁-cofiltered limits
has ℵ₁-filtered colimits

…it has colimits of the opposite shape, in order to resolve a property of Eff

ScriptRaccoon · 2026-09-08T23:27:39Z

Thanks! I will have a look.

Is the PR ready for review already?

It would be cool to prove that Eff has no generating set (which has been claimed here). Currently, CatDat does not have an example of an elementary topos that does not have a generating set.

dschepler · 2026-09-09T02:12:16Z

I think it's probably mostly ready for review - though there is one spot where we still need to find a reference (or else expand to a full proof of the elementary topos properties).

At the link, my understanding was the claim is that the effective topos doesn't have a small dense subcategory. I'd certainly believe that since I think I can prove the only coproducts which exist are the ones where all but finitely many terms are empty. It might be possible to extend that to a proof that the only colimits which exist are the ones which are more or less equivalent to a finite colimit, but I'm not sure about a formal formulation or proof of that.

That would still, of course, be sufficient to prove that it is not accessible, and it looks like we currently don't have an example of an elementary topos which is not accessible.

ScriptRaccoon · 2026-09-09T06:49:57Z

though there is one spot where we still need to find a reference

Yes and I think it's a reference for the most important property. Please try to locate it.

…omorphisms, inspired by a discussion in that reference

dschepler · 2026-09-10T00:21:20Z

I've found a reference https://www.sciencedirect.com/science/article/pii/S0022404905001593 which claims in passing "it is relatively easy to see" the collection of countable projectives is a generating set for Eff - though I don't see the "relatively easy" proof myself.

ScriptRaccoon · 2026-09-10T09:18:59Z

I've found a reference https://www.sciencedirect.com/science/article/pii/S0022404905001593 which claims in passing "it is relatively easy to see" the collection of countable projectives is a generating set for Eff - though I don't see the "relatively easy" proof myself.

In such cases, we can already add a proof to CatDat with the reference, along with a TODO comment to explain this more directly since the proof is incomplete. CatDat also aims to record what is known in the literature even if we do not understand everything.

I have not begun to read the changes in this PR, but I will do that tomorrow.

…tomatically extremal

ScriptRaccoon · 2026-09-11T13:41:12Z

+  - property: natural numbers object
+    proof: 'We claim that $N \coloneqq (\IN, \{ (n, n, n) \mid n \in \IN \})$ is a natural numbers object. To see this, suppose we have an object $(X, E_X)$ with morphisms $x : 1 \to X$ and $f : X \to X$. Then we can find $n_0 \in \IN, x_0 \in X$ such that $n_0 \Vdash 0 \xmapsto{x} x_0$; also, let $c$ and $t$ be witnesses to the codomain property and totality of $f$, respectively. We can then define an "iteration of $c\circ t$" program encoded by $i\in\IN$, such that $i \cdot n$ represents the result of the $n$-fold iteration of $t$ followed by $c$, starting with $c \cdot n_0$. We can also find a sequence $x_n \in X$ extending $x_0$ such that $t \cdot (i \cdot n) \Vdash x_n \xmapsto{f} x_{n+1}$. We can then show that $\{ (\langle n, m \rangle, n, y) \mid (m \Vdash x_n = y) \}$ is an effective functional relation which induces a morphism $N \to X$, and this morphism has the required properties. Likewise, the uniqueness of this morphism is straightforward to establish.'
+
+  - property: generating set


ℹ️ This needs to be changed to generating collection after #367 is merged. The proof does not change much.

ScriptRaccoon · 2026-09-11T15:26:20Z

ℹ️ Once you rebase on main and run pnpm db:update, this will add the effective topos to a JSON file (structure.history.json). Please commit the change.

ScriptRaccoon · 2026-09-11T15:34:12Z

+notation: $\Eff$
+objects: A set $X$ along with a subset $E_X \subseteq \IN \times X \times X$ giving an effective partial equivalence relation (see below for precise definition)
+morphisms: A morphism $(X, E_X) \to (Y, E_Y)$ is a subset $f \subseteq \IN \times X \times Y$ giving an effective functional relation, modulo a certain equivalence relation (see below for precise definitions)
+description: >-


This description is very detailed and maybe should be moved to the nLab. The other entries also refer for more detailed descriptions to the nLab (or other sources).

I did something similar with the category http://localhost:5173/category/cocompletion-discrete-pair-join, but this was a different situation since this category does not even deserve an nLab article.

If you agree to move it, of course, the description here does not need to repeat it. But please apply the changes suggested in the other comments first.

I could certainly move it to content/ . I found the descriptions at nLab to be very abstract and spread across multiple pages, which is part of why it took me so long to decode the definitions into this more concrete form for this specific case - so I'm not sure if a reference to nLab would be useful for giving the definitions.

I see. I see nLab as the major online reference for category theory. CatDat should not be competition. I want that CatDat is the place that records structured data of categories and other categorical structures. When a comprehensive and self-contained definition of the effective topos is missing, this is material for nLab. More people will find it (via google etc.) and profit from it. Either the existing article can be edited, or a separate article can be created (like Todd did for ETCS years ago).

I'm not sure about that. I don't see many nLab pages that have detailed proofs of everything, more often pages with overviews of the important properties and results, with maybe a few select proofs to be highlighted.

Though I could certainly register for an nLab account, start off by editing the "quasitopos" page with the correction of "generating set" to "strong generating set" (in nLab terminology) that we discovered a while ago, and then see if I can start a discussion of whether and/or where it could be appropriate to add such a thing.

In the meantime, I think it might help to start with the category of $\omega$-sets, which uses a lot of the same ingredients but the definitions are simpler. (In that category, an object is a set $X$ along with a "realizes" relation which is a subset of $\mathbb{N} \times X$ such that every $x \in X$ is realized by some $n\in \mathbb{N}$, and a morphism is a function $f : X \to Y$ such that there exists a partial recursive function $\varphi : \mathbb{N} \to \mathbb{N}$ such that whenever $n$ realizes $x$, then $\varphi(n) \downarrow$ and $\varphi(n)$ realizes $f(x)$. Then the effective topos could be viewed as freely adding quotients of congruences; even though the category of $\omega$-sets does have quotients of congruences already, they aren't effective quotients in general, and re-adding quotients turns out to make those quotients effective and result in a topos.)

I'm not sure about that. I don't see many nLab pages that have detailed proofs of everything

That is true. But some pages have very long and detailed proofs, too. But notice that I was only suggesting to put the detailed definition to the nLab. The only required proof is that the result is a category (thus, answering my other questions).

Though I could certainly register for an nLab account

No account is required. You can click on "Edit" and go ahead. Just enter your name in the textbox and submit. 👍🏻

In the meantime, I think it might help to start with the category of ω-sets

This sounds like a really good idea.

OK, I've created a new branch dschepler/CatDat/omega-set and I'll start working on populating that for now.

ScriptRaccoon · 2026-09-11T15:40:44Z

+  * (Symmetry:) There exists $s \in \IN$ such that whenever $n \Vdash x_1 = x_2$, then $s \cdot n \downarrow$ and $s \cdot n \Vdash x_2 = x_1$.
+
+  * (Transitivity:) There exists $t \in \IN$ such that whenever $n \Vdash x_1 = x_2$ and $m \Vdash x_2 = x_3$, then $t \cdot \langle n, m \rangle \downarrow$ and $t \cdot \langle n, m \rangle \Vdash x_1 = x_3$.
+


Why is reflexivity missing?

That's intentional. A value witnessing $x = x$ is meant to represent a certificate that $x$ is a "valid" member of the type. It could sort of be viewed as a parallel to forcing, where a name of a set in the forcing model includes conditions under which certain things are added as elements of the set.

Ok. In any writeup of the whole thing (either as content page or, what I would prefer, nLab page), things like this deserve a whole paragraph. Here, where a category should be defined briefly, it needs to be omitted, I am afraid.

ScriptRaccoon · 2026-09-11T15:53:00Z

+
+  To give a precise definition, first fix a certain Turing-equivalent theory of computation, with an encoding of programs as elements of $\IN$ (note that not every element of $\IN$ needs to be a valid program encoding). We also fix a pairing function $\langle {-}, {-} \rangle : \IN \xrightarrow{\sim} \IN \times \IN$ along with the inverse pair $p_1, p_2 : \IN \rightrightarrows \IN$. We will define notation $p \cdot n \downarrow$ to mean that $p$ is a valid program encoding, and running the corresponding program with input $n$ terminates without error, returning a value $p \cdot n$.
+
+  Given a subset $E_X \subseteq \IN \times X \times X$, we will use notation $n \Vdash x_1 = x_2$ (or informally, $n$ realizes equality of $x_1$ and $x_2$) to mean $(n, x_1, x_2) \in E_X$. We will say that $E_X$ is an <i>effective partial equivalence relation</i> if $(p_1)_*(E_X)$ is a partial equivalence relation on $X$ with partial recursive functions relating the corresponding realizers; namely:


How can a natural number model an equality x = y? What is the picture in the computing analogy? Is the natural number an encoding of a proof?

And what is $E_X$ then, intuitively?

In order to form a topos, you need to be able to take quotients of effective equivalence relations. Without the quotients, what you get are called $\omega$-sets -- or "assemblies of the first Kleene combinatory algebra" or "assemblies" for short if clear from context -- and that category looks like it's only a quasitopos (I saw a result in one of the articles I browsed that it's in fact equivalent to the $\lnot\lnot$-separated objects of Eff). So, we also allow for "certificates" of some sort that two values are to be considered equivalent.

(And then, allowing for partial equivalence relations which for some $x\in X$ have no witnesses at all that $x$ is valid is a matter of convenience for some of the constructions.)

Maybe it could help if I replace $n \Vdash x = y$ with $n \Vdash x \equiv y$? And perhaps use some special notation for $n \Vdash x \equiv x$ such as $n \Vdash x \downarrow$ to emphasize that we're considering it as a sort of "validity predicate"?

Ok. Yeah adding $\omega$-sets probably will clarify lots of things.

Yes, I prefer $n \models x \equiv y$ over $n \models x = y$. And when you introduce that notation, it will be definitely helpful to also explain what you did just here.

I don't like to have another notation for $n \models x \equiv x$, but it will be helpful to explain in 1-2 sentences what it means intuitively.

ScriptRaccoon · 2026-09-11T15:59:29Z

+
+  * Conversely, there exists $\ell_2$ such that whenever $n \Vdash x \xmapsto{g} y$, then $\ell_2 \cdot n \downarrow$ and $\ell_2 \cdot n \Vdash x \xmapsto{f} y$.
+
+  The effective topos is then defined to be the category whose objects are pairs $(X, E_X)$ where $X$ is a set and $E_X$ is an effective partial equivalence relation on $X$; and the morphisms $\Hom((X, E_X), (Y, E_Y))$ are the quotient of the set of effective functional relations by the equivalence relation defined above. The identity morphism of $(X, E_X)$ is the equivalence class of $E_X$; in other words, it is $[\id]$ where $n \Vdash x \xmapsto{\id} y$ if and only if $n \Vdash x = y$. Composition is defined such that for $f$ an effective functional relation between $(Y, E_Y)$ and $(Z, E_Z)$ and $g$ an effective functional relation between $(X, E_X)$ and $(Y, E_Y)$, $[f] \circ [g]$ is the equivalence class of $f \circ g \coloneqq \{ (\langle n, m\rangle, x, z) \mid \exists y\in Y, (n \Vdash x \xmapsto{g} y) \land (m \Vdash y \xmapsto{f} z) \}$.


Why is composition well-defined? Why are the two category axioms satisfied? Please add a reference. (I think the proofs are too long to be written down here. Maybe on a content page it would work, or the nLab article.)

ScriptRaccoon · 2026-09-11T16:04:48Z

+    proof: This is trivial.
+
+  - property: elementary topos
+    proof: This is a special case of the fact that from any <a href="https://ncatlab.org/nlab/show/tripos">tripos</a> we can construct a topos. See for example <a href="https://www.cl.cam.ac.uk/~amp12/papers/thet/thet.pdf">A. M. Pitts, <i>The Theory of Triposes</i></a>, with the definition of effective tripos in section 1.5 on p. 16, and the construction of a topos corresponding to a tripos as Thm. 2.3.


It is a bit unfortunate that readers, in particular those who are not familiar with the whole theory (like myself), after reading the long and complicated definition of the effective topos, which even left out some details, now stumble upon another notion, that of a tripos and need to understand it from the references. The relation is also not immediately clear to me. Which tripos do we use here? And why do we get the effective topos in that example? More importantly, why are we even using the long-winded definition above then?

I will stop reading for now, since I first need to understand more basic things before being able to understand any of the following proofs.

You have a point - similarly to the way I found I needed to digest the abstract definitions into a more concrete definition for this case, it would probably be useful to write up this special case of the proofs as well.

…rating collection

ScriptRaccoon · 2026-09-13T20:25:02Z

+- id: topos_generating_set_implies_cogenerating_set
+  assumptions:
+    - elementary topos
+    - generating set


*generating collection

I assume this is also why the tests fail.

dschepler added 2 commits September 8, 2026 17:58

Add the effective topos

bd3f36d

Add several instances of topos has limits of a certain shape implies …

48c7a0a

…it has colimits of the opposite shape, in order to resolve a property of Eff

ScriptRaccoon added the data label Sep 8, 2026

ScriptRaccoon linked an issue Sep 8, 2026 that may be closed by this pull request

Add effective topos #353

Open

dschepler added 2 commits September 9, 2026 18:10

Add reference for proof Eff is a topos; also expand description of is…

2b59fc2

…omorphisms, inspired by a discussion in that reference

Small fix to natural numbers object proof

d4d8dd1

dschepler added 2 commits September 10, 2026 08:59

Add proof that Eff has an extremal generating set

a098b4b

Simplify: I forgot that generating sets in a balanced category are au…

8ff10c9

…tomatically extremal