From bd3f36d8003adee18f4dbc9e332c17a7f434021d Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Tue, 8 Sep 2026 17:58:27 -0400 Subject: [PATCH 1/9] Add the effective topos --- .cspell.json | 1 + database/data/categories/Eff.yaml | 142 ++++++++++++++++++++++++++++++ database/data/config.yaml | 1 + database/data/macros.yaml | 1 + 4 files changed, 145 insertions(+) create mode 100644 database/data/categories/Eff.yaml diff --git a/.cspell.json b/.cspell.json index ea713a958..0093f53e7 100644 --- a/.cspell.json +++ b/.cspell.json @@ -224,6 +224,7 @@ "injections", "injective", "injectivity", + "intuitionistic", "invertibility", "Isbell", "isos", diff --git a/database/data/categories/Eff.yaml b/database/data/categories/Eff.yaml new file mode 100644 index 000000000..96010c227 --- /dev/null +++ b/database/data/categories/Eff.yaml @@ -0,0 +1,142 @@ +id: Eff +name: effective topos +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: >- + The effective topos gives a "realizability" model of first-order intuitionistic logic roughly matching the principles of constructive mathematics — for example, that a proof of existence requires a computable function on the inputs whose output is a witness of the property, and similarly that a proof of a disjunction requires a computation (based on inputs from the context) of which branch of the disjunction holds. For instance, in this model, every total function $\IN \to \IN$ is (internally) recursive. Similarly, in the resulting model of constructive analysis, it turns out that every total function $\IR \to \IR$ on the constructive reals is continuous; and the Intermediate Value Theorem fails. + + 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 effective partial equivalence relation if $(p_1)_*(E_X)$ is a partial equivalence relation on $X$ with partial recursive functions relating the corresponding realizers; namely: + + * (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$. + + Likewise, suppose $f \subseteq \IN \times X \times Y$ where we have fixed effective partial equivalence relations $E_X$ and $E_Y$ on $X$ and $Y$, respectively. We then use notation $n \Vdash x \xmapsto{f} y$ to mean $(n, x, y) \in f$. We will say $f$ is an effective functional relation if $(p_1)_*(f)$ is a functional relation $X / E_X \to Y / E_Y$, with partial recursive functions relating the corresponding realizers; namely: + + * (Domain condition:) There exists $d \in \IN$ such that whenever $n \Vdash x \xmapsto{f} y$, then $d \cdot n \downarrow$ and $d \cdot n \Vdash x = x$. + + * (Codomain condition:) There exists $c \in \IN$ such that whenever $n \Vdash x \xmapsto{f} y$, then $c \cdot n \downarrow$ and $c \cdot n \Vdash y = y$. + + * (Respectfulness condition:) There exists $r \in \IN$ such that whenever $n \Vdash x_1 \xmapsto{f} y_1$, $m \Vdash x_1 = x_2$, and $p \Vdash y_1 = y_2$, then $r \cdot \langle \langle n, m \rangle, p \rangle \downarrow$ and $r \cdot \langle \langle n, m \rangle, p \rangle \Vdash x_2 \xmapsto{f} y_2$. (From now on, we will use $\langle n, m, p \rangle$ as shorthand for $\langle \langle n, m \rangle, p \rangle$, with projectors $p_{1/3} \coloneqq p_1 \circ p_1$, $p_{2/3} \coloneqq p_2 \circ p_1$, $p_{3/3} \coloneqq p_2$; and similarly for larger tuples.) + + * (Image uniqueness condition:) There exists $u \in \IN$ such that whenever $n \Vdash x \xmapsto{f} y_1$ and $m \Vdash x \xmapsto{f} y_2$, then $u \cdot \langle n, m \rangle \downarrow$ and $u \cdot \langle n, m \rangle \Vdash y_1 = y_2$. + + * (Totality condition:) There exists $t \in \IN$ such that whenever $n \Vdash x = x$, then $t \cdot n \downarrow$, and there exists $y \in Y$ such that $t \cdot n \Vdash x \xmapsto{f} y$. + + Similarly, for two such functional relations $f$ and $g$, we will say $f$ and $g$ are equivalent if $(p_1)_*(f) = (p_1)_*(g)$, with partial recursive functions relating the corresponding realizers; namely: + + * There exists $\ell_1$ such that whenever $n \Vdash x \xmapsto{f} y$, then $\ell_1 \cdot n \downarrow$ and $\ell_1 \cdot n \Vdash x \xmapsto{g} y$. + + * 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) \}$. + +nlab_link: https://ncatlab.org/nlab/show/effective+topos + +tags: + - computation theory + +related: + - Set + +satisfied_properties: + - property: locally small + proof: This is trivial. + + - property: elementary topos + proof: This is a special case of the fact that from any tripos we can construct a topos. (Needs reference...) + + - property: semi-strongly connected + proof: Suppose we have two objects $(X, E_X)$ and $(Y, E_Y)$. If $E_Y$ is non-empty, then we can find $n_0\in \IN, y_0\in Y$ such that $n_0 \Vdash y_0 = y_0$. Then $\{ (\langle n, m \rangle, x, y) \mid (n \Vdash x = x) \land (m \Vdash y = y_0) \}$ gives an effective functional relation which induces a morphism $(X, E_X) \to (Y, E_Y)$. (This represents a constant morphism with value $y_0$.) Otherwise, if $E_Y$ is empty, then $\varnothing$ induces a morphism $(Y, E_Y) \to (X, E_X)$. + + - 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 x_0 = 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 $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.' + +unsatisfied_properties: + - property: skeletal + proof: Consider $(X, \IN \times \Delta_X)$ and $(Y, \IN \times \Delta_Y)$ for bijective but unequal sets $X, Y$. + + - property: countable copowers + proof: If there were an $\aleph_0$-indexed copower of the terminal object, it would be isomorphic to the natural numbers object $N$ by this result, and any function $\IN \to \IN$ would induce a morphism $N \to N$. However, every morphism $N \to N$ in fact induces a total recursive function $\IN \to \IN$ on the global sections (in fact, the function on global sections agrees with the witness $t$ of totality for a representative of the equivalence class). We therefore get a contradiction from the fact that not every function $\IN \to \IN$ is recursive. + + - property: essentially small + proof: 'There is a fully faithful (and therefore conservative) functor $\Set \to \Eff$ which sends $X$ to $(X, \IN \times \Delta_X)$, and which sends $f : X \to Y$ to the equivalence class of $\IN \times \Gamma_f$ where $\Gamma_f$ is the graph of $f$.' + + - property: locally finite + proof: For example, $\Hom(1, N)$ is countably infinite where $N$ is the natural numbers object. + +special_objects: + initial object: + description: $(\varnothing, \varnothing)$ + terminal object: + description: $(1, \{ (0, 0, n) \mid n \in \IN \})$ + coproducts: + description: The binary coproduct of $(X, E_X)$ and $(Y, E_Y)$ is $X \sqcup Y$ with the PER given by $\{ (2n, x_1, x_2) \in \IN \times X \times X \mid n \Vdash x_1 = x_2 \} \cup \{ (2n+1, y_1, y_2) \in \IN \times Y \times Y \mid n \Vdash y_1 = y_2 \}$. + products: + description: The binary product of $(X, E_X)$ and $(Y, E_Y)$ is $X \times Y$ with the PER given by $\{ (\langle n, m \rangle, (x_1, y_1), (x_2, y_2)) \mid (n \Vdash x_1 = x_2) \land (m \Vdash y_1 = y_2) \}$ + +special_morphisms: + isomorphisms: + description: A morphism is an isomorphism if and only if it is a monomorphism and an epimorphism (see below). + proof: Being an elementary topos, $\Eff$ is balanced. + monomorphisms: + description: For an effective functional relation $f \subseteq \IN \times X \times Y$, the equivalence class of $f$ is a monomorphism if and only if there is $i\in\IN$ such that whenever $n \Vdash x_1 \xmapsto{f} y$ and $m \Vdash x_2 \xmapsto{f} y$, then $i \cdot \langle n, m \rangle \downarrow$ and $i \cdot \langle n, m \rangle \Vdash x_1 = x_2$. + proof: >- + ($\Rightarrow$) We can define a kernel pair $E$ of $f$ with underlying set $X\times X$, and partial equivalence relation $\{ (\langle n, m, p, q \rangle, (x_1, x_2), (x_3, x_4)) \mid \exists y\in Y, (n \Vdash x_1 = x_3) \land (m \Vdash x_2 = x_4) \land (p \Vdash x_1 \xmapsto{f} y) \land (q \Vdash x_2 \xmapsto{f} y) \}$. We can also construct $[\pi_1], [\pi_2] : E \rightrightarrows (X, E_X)$ where $\pi_1$ is the effective functional relation $\{ (\langle n, m, p\rangle, (x_1, x_2), x_3) \mid \exists y\in Y, (n \Vdash x_1 \xmapsto{f} y) \land (m \Vdash x_2 \xmapsto{f} y) \land (p \Vdash x_1 = x_3) \}$, and similarly for $\pi_2$ with the last condition replaced with $p \Vdash x_2 = x_3$. We can then check $[f] \circ [\pi_1] = [f] \circ [\pi_2]$. Since $[f]$ is a monomorphism, we conclude $[\pi_1] = [\pi_2]$. Say we have witnesses $\ell_1, \ell_2$ to the equivalence of $\pi_1$ and $\pi_2$. + + Now, suppose we have $n \Vdash x_1 \xmapsto{f} y$ and $m \Vdash x_2 \xmapsto{f} y$. Then + $$\begin{align*} & n_1 \Vdash (x_1, x_2) \xmapsto{\pi_1} x_1 & n_1 & \coloneqq \langle n, m, d_f \cdot n \rangle \\ + \implies & n_2 \Vdash (x_1, x_2) \xmapsto{\pi_2} x_1 & n_2 & \coloneqq \ell_1 \cdot n_1 \\ + \implies & n_3 \Vdash x_2 = x_1 & n_3 & \coloneqq p_2(n_2) \\ + \implies & n_4 \Vdash x_1 = x_2 & n_4 & \coloneqq s_X \cdot n_3.\end{align*}$$ + It is now easy to write a program which transforms $\langle n, m \rangle$ into $n_4$ following the steps in the right column, and an encoding of this program gives the required $i$. + + ($\Leftarrow$) Essentially, we adapt the proof that an injective function is a monomorphism in $\Set$, and carry along realizers through the proof, verifying in the end that the transformation of realizers is computable. In detail, suppose we have an object $(Z, E_Z)$ and morphisms $[g], [h] : (Z, E_Z) \to (X, E_X)$ such that $[f] \circ [g] = [f] \circ [h]$ with witnesses $\ell_1, \ell_2 \in \IN$. Then whenever $n \Vdash z \xmapsto{g} x$, we have + $$\begin{align*} & n_1 \Vdash x = x & n_1 & \coloneqq c_g \cdot n. \end{align*}$$ + Thus, there exists $y \in Y$ such that + $$\begin{align*} & n_2 \Vdash x \xmapsto{f} y & n_2 & \coloneqq t_f \cdot n_1 \\ + \implies & n_3 \Vdash z \xmapsto{f\circ g} y & n_3 & \coloneqq \langle n, n_2 \rangle \\ + \implies & n_4 \Vdash z \xmapsto{f\circ h} y & n_4 & \coloneqq \ell_1 \cdot n_3. \end{align*}$$ + By the definition of $f \circ h$, there exists $x' \in X$ such that + $$\begin{align*} & n_5 \Vdash z \xmapsto{h} x', & n_5 & \coloneqq p_1(n_4) \\ + & n_6 \Vdash x' \xmapsto{f} y & n_6 & \coloneqq p_2(n_4) \\ + \implies & n_7 \Vdash x' = x & n_7 & \coloneqq i \cdot \langle n_6, n_2 \rangle \\ + \implies & n_8 \Vdash z \xmapsto{h} x & n_8 & \coloneqq r_h \cdot \langle n_5, d_g \cdot n, n_7 \rangle. \end{align*}$$ + It is now easy to write a program which transforms $n$ into $n_8$ according to the steps in the right column, and an encoding of this program gives the first half of the witness pair to $[g] = [h]$. The second half is almost identical, just swapping the roles of $g$ and $h$. + epimorphisms: + description: For an effective functional relation $f \subseteq \IN \times X \times Y$, the equivalence class of $f$ is an epimorphism if and only if there is $s\in\IN$ such that whenever $n \Vdash y = y$, then $s \cdot n \downarrow$ and there exists $x \in X$ such that $s \cdot n \Vdash x \xmapsto{f} y$. + proof: >- + ($\Rightarrow$) We will define $Z$ to be $Y \sqcup \{ * \}$ with every member of the image of $f$ identified with $*$; namely, + $$\begin{align*} E_Z \coloneqq & \{ (0, *, *) \} \cup\\ + & \{ (4n+1, y_1, y_2) \mid n \Vdash y_1 = y_2 \} \cup\\ + & \{ (4n+2, y_1, *) \mid \exists x\in X, n \Vdash x \xmapsto{f} y_1 \} \cup\\ + & \{ (4n+3, *, y_2) \mid \exists x\in X, n \Vdash x \xmapsto{f} y_2 \} \cup\\ + & \{ (4 \langle n, m \rangle + 4, y_1, y_2) \mid \exists x_1, x_2\in X, (n \Vdash x_1 \xmapsto{f} y_1) \land (m \Vdash x_2 \xmapsto{f} y_2) \}.\end{align*}$$ + We can also define two effective functional relations $g$ and $h$ representing the projection and the constant map with value *, respectively. Namely, $g \coloneqq \{ (n, y, z) \mid n \Vdash y =_Z z \}$ and $h \coloneqq \{ (n, y, *) \mid n \Vdash y =_Y y \}$. We can check that $[g] \circ [f] = [h] \circ [f]$. Therefore, since $[f]$ is an epimorphism, we have $[g] = [h]$. Say we have witnesses $\ell_1, \ell_2$ to the equivalence of $g$ and $h$. + + Now, suppose we have $n \Vdash y =_Y y$. Then + $$\begin{align*} & n_1 \Vdash y \xmapsto{g} y & n_1 & \coloneqq n \\ + \implies & n_2 \Vdash y \xmapsto{h} y & n_2 & \coloneqq \ell_1 \cdot n_1.\end{align*}$$ + We also have + $$\begin{align*} & n_3 \Vdash y \xmapsto{h} * & n_3 & \coloneqq n \\ + \implies & n_4 \Vdash y = * & n_4 & \coloneqq u \cdot \langle n_2, n_3 \rangle.\end{align*}$$ + In this last statement, the only possibility for $y$ to be identified with $*$ in $Z$ is for $n_4$ to be of the form $4n_5 + 2$, with the existence of $x\in X$ such that + $$\begin{align*} & n_5 \Vdash x \xmapsto{f} y & n_5 & \coloneqq \frac{n_4-2}{4}.\end{align*}$$ + It is now easy to write a program which transforms $n$ into $n_5$ following the steps in the right column (in case $n_4$ is not of the required form, we can have the program either signal an error, intentionally enter an infinite loop, or proceed with an arbitrary value for $n_5$). An encoding of this program gives the required $s$. + + ($\Leftarrow$) Essentially, we adapt the proof that a surjective function is an epimorphism in $\Set$, and carry along realizers through the proof, verifying in the end that the transformation of realizers is computable. In detail, suppose we have an object $(Z, E_Z)$ and morphisms $[g], [h] : (Y, E_Y) \to (Z, E_Z)$ such that $[g] \circ [f] = [h] \circ [f]$ with witnesses $\ell_1, \ell_2 \in \IN$. Then whenever $n \Vdash y \xmapsto{g} z$, we have + $$\begin{align*} & n_1 \Vdash y = y & n_1 & \coloneqq d_g \cdot n. \end{align*}$$ + Thus, by assumption there exists $x\in X$ such that + $$\begin{align*} & n_2 \Vdash x \xmapsto{f} y & n_2 & \coloneqq s \cdot n_1 \\ + \implies & n_3 \Vdash x \xmapsto{g\circ f} z & n_3 & \coloneqq \langle n_2, n \rangle \\ + \implies & n_4 \Vdash x \xmapsto{h\circ f} z & n_4 & \coloneqq \ell_1 \cdot n_3.\end{align*}$$ + By definition of $h\circ f$, then, there exists $y' \in Y$ such that + $$\begin{align*} & n_5 \Vdash x \xmapsto{f} y', & n_5 & \coloneqq p_1(n_4) \\ + & n_6 \Vdash y' \xmapsto{h} z & n_6 & \coloneqq p_2(n_4) \\ + \implies & n_7 \Vdash y' = y & n_7 & \coloneqq u_f \cdot \langle n_5, n_2 \rangle \\ + \implies & n_8 \Vdash z = z & n_8 & \coloneqq c_g \cdot n \\ + \implies & n_9 \Vdash y \xmapsto{h} z & n_9 & \coloneqq r_h \cdot \langle n_6, n_7, n_8 \rangle.\end{align*}$$ + It is now easy to write a program which transforms $n$ into $n_9$ according to the steps in the right column, and an encoding of this program gives the first half of the witness pair to $[g] = [h]$. The second half is almost identical, just swapping the roles of $g$ and $h$. diff --git a/database/data/config.yaml b/database/data/config.yaml index 391bea0d8..b20576377 100644 --- a/database/data/config.yaml +++ b/database/data/config.yaml @@ -4,6 +4,7 @@ structure_tags: - analysis - category theory - combinatorics + - computation theory - number theory - order theory - set theory diff --git a/database/data/macros.yaml b/database/data/macros.yaml index 29b86f363..ef54e0e87 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -151,3 +151,4 @@ \Mono: \mathbf{Mono} \Sh: \mathbf{Sh} \Proj: \mathbf{Proj} +\Eff: \mathbf{Eff} From 48c7a0a5f56b0201429dbd9c59302189d10ac30f Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Tue, 8 Sep 2026 17:59:24 -0400 Subject: [PATCH 2/9] Add several instances of topos has limits of a certain shape implies it has colimits of the opposite shape, in order to resolve a property of Eff --- .../data/category-implications/topos.yaml | 72 +++++++++++++++++++ 1 file changed, 72 insertions(+) diff --git a/database/data/category-implications/topos.yaml b/database/data/category-implications/topos.yaml index 05a89d3eb..caa5c14ea 100644 --- a/database/data/category-implications/topos.yaml +++ b/database/data/category-implications/topos.yaml @@ -35,6 +35,78 @@ - coregular proof: This is proven in Johnstone, A2.6.3. +- id: topos_monadic_over_itself + assumptions: + - elementary topos + - complete + conclusions: + - cocomplete + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + +- id: topos_monadic_over_itself_countable_powers + assumptions: + - elementary topos + - countable powers + conclusions: + - countable copowers + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + +- id: topos_monadic_over_itself_sequential + assumptions: + - elementary topos + - sequential limits + conclusions: + - sequential colimits + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + +- id: topos_monadic_over_itself_sifted + assumptions: + - elementary topos + - cosifted limits + conclusions: + - sifted colimits + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + +- id: topos_monadic_over_itself_directed + assumptions: + - elementary topos + - directed limits + conclusions: + - directed colimits + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + +- id: topos_monadic_over_itself_filtered + assumptions: + - elementary topos + - cofiltered limits + conclusions: + - filtered colimits + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + +- id: topos_monadic_over_itself_aleph1_filtered + assumptions: + - elementary topos + - ℵ₁-cofiltered limits + conclusions: + - ℵ₁-filtered colimits + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + +- id: topos_monadic_over_itself_aleph2_powers + assumptions: + - elementary topos + - ℵ₂-small powers + conclusions: + - ℵ₂-small copowers + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + +- id: topos_monadic_over_itself_aleph2 + assumptions: + - elementary topos + - ℵ₂-small products + conclusions: + - ℵ₂-small coproducts + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + - id: grothendieck_topos_definition assumptions: - Grothendieck topos From 2b59fc28d247837c2e50e442a14fd12eed94eceb Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Wed, 9 Sep 2026 18:10:23 -0400 Subject: [PATCH 3/9] Add reference for proof Eff is a topos; also expand description of isomorphisms, inspired by a discussion in that reference --- database/data/categories/Eff.yaml | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/database/data/categories/Eff.yaml b/database/data/categories/Eff.yaml index 96010c227..005abc645 100644 --- a/database/data/categories/Eff.yaml +++ b/database/data/categories/Eff.yaml @@ -47,7 +47,7 @@ satisfied_properties: proof: This is trivial. - property: elementary topos - proof: This is a special case of the fact that from any tripos we can construct a topos. (Needs reference...) + proof: This is a special case of the fact that from any tripos we can construct a topos. See for example A. M. Pitts, The Theory of Triposes, 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. - property: semi-strongly connected proof: Suppose we have two objects $(X, E_X)$ and $(Y, E_Y)$. If $E_Y$ is non-empty, then we can find $n_0\in \IN, y_0\in Y$ such that $n_0 \Vdash y_0 = y_0$. Then $\{ (\langle n, m \rangle, x, y) \mid (n \Vdash x = x) \land (m \Vdash y = y_0) \}$ gives an effective functional relation which induces a morphism $(X, E_X) \to (Y, E_Y)$. (This represents a constant morphism with value $y_0$.) Otherwise, if $E_Y$ is empty, then $\varnothing$ induces a morphism $(Y, E_Y) \to (X, E_X)$. @@ -80,8 +80,17 @@ special_objects: special_morphisms: isomorphisms: - description: A morphism is an isomorphism if and only if it is a monomorphism and an epimorphism (see below). - proof: Being an elementary topos, $\Eff$ is balanced. + description: For an effective functional relation $f \subseteq \IN \times X \times Y$, the equivalence class of $f$ is an isomorphism if and only if the inverse relation $f^{-1} \subseteq \IN \times Y \times X$ is also an effective functional relation; or equivalently, if $[f]$ is both a monomorphism and an epimorphism (see below). + proof: >- + The equivalence to $f$ being a monomorphism and an epimorphism follows from the fact that the effective topos is an elementary topos, and therefore balanced. + + ($\Rightarrow$) Most of the conditions for $f^{-1}$ being an effective functional relation are automatic. In establishing the uniqueness of image condition for $f^{-1}$, we use the fact that $f$ is a monomorphism and the description below. Similarly, in establishing the totality condition for $f^{-1}$, we use the fact that $f$ is an epimorphism and the description below. + + Alternately, if $[g]$ is an inverse to $[f]$, so that $f \circ g$ and $g \circ f$ are equivalent to the identities, it is straightforward to show that $f^{-1}$ satisfies the definition of being equivalent to $g$ (ignoring for the moment that we haven't yet established $f^{-1}$ is effective functional), and then use this along with the fact that $g$ is effective functional to show $f^{-1}$ is also effective functional. + + ($\Leftarrow$) The effective topos being an elementary topos and therefore balanced, it is sufficient to show $f$ is a monomorphism and an epimorphism. The fact that $f$ is a monomorphism follows from the uniqueness of image condition and $f^{-1}$ and the description of monomorphisms below. Similarly, the fact that $f$ is an epimorphism follows from the totality condition for $f^{-1}$ and the description of epimorphisms below. + + Alternately, assuming $f^{-1}$ is effective functional, then it is staightforward to show that $f \circ f^{-1}$ and $f^{-1} \circ f$ are equivalent to the identities, so that $[f^{-1}]$ forms an inverse to $[f]$. monomorphisms: description: For an effective functional relation $f \subseteq \IN \times X \times Y$, the equivalence class of $f$ is a monomorphism if and only if there is $i\in\IN$ such that whenever $n \Vdash x_1 \xmapsto{f} y$ and $m \Vdash x_2 \xmapsto{f} y$, then $i \cdot \langle n, m \rangle \downarrow$ and $i \cdot \langle n, m \rangle \Vdash x_1 = x_2$. proof: >- From d4d8dd1af19bf55f5847f5b7f13176a574c6c9db Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Wed, 9 Sep 2026 18:33:36 -0400 Subject: [PATCH 4/9] Small fix to natural numbers object proof --- database/data/categories/Eff.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/database/data/categories/Eff.yaml b/database/data/categories/Eff.yaml index 005abc645..a212a1f40 100644 --- a/database/data/categories/Eff.yaml +++ b/database/data/categories/Eff.yaml @@ -53,7 +53,7 @@ satisfied_properties: proof: Suppose we have two objects $(X, E_X)$ and $(Y, E_Y)$. If $E_Y$ is non-empty, then we can find $n_0\in \IN, y_0\in Y$ such that $n_0 \Vdash y_0 = y_0$. Then $\{ (\langle n, m \rangle, x, y) \mid (n \Vdash x = x) \land (m \Vdash y = y_0) \}$ gives an effective functional relation which induces a morphism $(X, E_X) \to (Y, E_Y)$. (This represents a constant morphism with value $y_0$.) Otherwise, if $E_Y$ is empty, then $\varnothing$ induces a morphism $(Y, E_Y) \to (X, E_X)$. - 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 x_0 = 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 $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.' + 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.' unsatisfied_properties: - property: skeletal From a098b4b562819e08dff96f51b6e40ac3c789e4bc Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Thu, 10 Sep 2026 08:59:56 -0400 Subject: [PATCH 5/9] Add proof that Eff has an extremal generating set --- database/data/categories/Eff.yaml | 36 +++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/database/data/categories/Eff.yaml b/database/data/categories/Eff.yaml index a212a1f40..333ef7eca 100644 --- a/database/data/categories/Eff.yaml +++ b/database/data/categories/Eff.yaml @@ -55,6 +55,42 @@ satisfied_properties: - 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: extremal generating set + proof: >- + We claim that the collection of all $(X, E_X)$ with $X \subseteq \IN$ forms an extremal generating set. First, to see it is a generating set, suppose we have two effective functional relations $f, g$ between $(X, E_X)$ and $(Y, E_Y)$ such that $[f] \ne [g]$. Then either a witness $\ell_1$ or a witness $\ell_2$ does not exist; without loss of generality, suppose $\ell_1$ does not exist. That means that for each $\ell \in \IN$, we can find $n_\ell \in \IN$ and $x_\ell \in X$, $y_\ell \in Y$ such that $n_\ell \Vdash x_\ell \xmapsto{f} y_\ell$ but either $\ell \cdot n_\ell \not\downarrow$ or $\ell \cdot n_ell \not\Vdash x_\ell \xmapsto{g} y_\ell$. In either case, make one such choice for each $\ell$, and let $X' \coloneqq \{ x_\ell \mid \ell \in \IN \}$, and $E_{X'} \coloneqq E_X \cap (\IN \times X' \times X')$. We can then check that $E_{X'}$ is an effective PER; $i \coloneqq E_X \cap (\IN \times X' \times X)$ is an effective functional relation inducing a morphism $[i] : (X', E_{X'}) \to (X, E_X)$. + + We now claim $[f] \circ [i] \ne [g] \circ [i]$. Suppose to the contrary that $f\circ i$ and $g\circ i$ were equivalent, with witnesses $\ell_1$ and $\ell_2$. Then whenever $x' \in X'$, and $n \Vdash x' \xmapsto{f} y$, we have: + $$\begin{align*} + & n_1 \Vdash x' = x' & n_1 & \coloneqq d_f \cdot n \\ + \implies & n_2 \Vdash x' \xmapsto{i} x' & n_2 & \coloneqq n_1 \\ + \implies & n_3 \Vdash x' \xmapsto{f\circ i} y & n_3 & \coloneqq \langle n_2, n \rangle \\ + \implies & n_4 \Vdash x' \xmapsto{g\circ i} y & n_4 & \coloneqq \ell_1 \cdot n_3 \\ + \implies \exists x_2\in X, ~ & n_5 \Vdash x' \xmapsto{i} x_2 & n_5 & \coloneqq p_1(n_4) \\ + & n_6 \Vdash x_2 \xmapsto{g} y & n_6 & \coloneqq p_2(n_4) \\ + \implies & n_7 \Vdash x' = x_2 & n_7 & \coloneqq n_5 \\ + \implies & n_8 \Vdash x' \xmapsto{g} y & n_8 & \coloneqq r_g \cdot \langle n_6, s_X \cdot n_7, c_f \cdot n \rangle.\end{align*}$$ + Therefore, if we let $\ell$ be the encoding of a program representing the transformation from $n$ to $n_8$ in the right column, then $n_\ell \Vdash x_\ell \xmapsto{f} y_\ell$; $\ell \cdot n_\ell \downarrow$; and $\ell \cdot n_\ell \Vdash x_\ell \xmapsto{g} y_\ell$. This contradicts the choice of $x_\ell$. + + On the other hand, $(X', E_{X'})$ is isomorphic to an object with $X' \subseteq \IN$ (in fact, structurally isomorphic, not just isomorphic in $\Eff$). + + Similarly, to show it is an extremal generating set, suppose we have an effective functional relation $f$ between $(X, E_X)$ and $(Y, E_Y)$ such that $[f]$ is not an isomorphism. By the above, if $[f]$ is not a monomorphism, then we can find $(U, E_U)$ with $U \subseteq \IN$ such that $\Hom(U, X) \to \Hom(U, Y)$ is not injective. Otherwise, since $\Eff$ is balanced, $[f]$ must not be an epimorphism. Using the description of epimorphisms below, we conclude that for each $s \in \IN$, there exists $n_s \in \IN$ and $y_s \in Y$ such that $n_s \Vdash y_s = y_s$, but either $s \cdot n_s \not\downarrow$ or for all $x \in X$, $s \cdot n_s \not\Vdash x \xmapsto{f} y_s$. In either case, make one such choice for each $s$, and let $Y' \coloneqq \{ y_s \mid s \in \IN \}$, $E_{Y'} \coloneqq E_Y \cap (\IN \times Y' \times Y')$, and $i \coloneqq E_Y \cap (\IN \times Y' \times Y)$. Then $E_{Y'}$ is an effective PER, $i$ is an effective functional relation inducing a morphism $[i] : (Y', E_{Y'}) \to (Y, E_Y)$. + + We now claim that the conditions above make it impossible for there to be a functional relation $g$ between $(Y', E_{Y'})$ and $(X, E_X)$ such that $[i] = [f] \circ [g]$, with witnesses $\ell_1$ and $\ell_2$ of the equivalence of $i$ and $f \circ g$. Suppose, to the contrary, we did have such a functional relation $g$. Then whenever $y' \in Y'$ and $n \Vdash y' = y'$, we have: + $$\begin{align*} + \exists x\in X, ~ & n_1 \Vdash y' \xmapsto{g} x & n_1 & \coloneqq t_g \cdot n \\ + \implies & n_2 \Vdash x = x & n_2 & \coloneqq c_g \cdot n_1 \\ + \implies \exists y\in Y, ~ & n_3 \Vdash x \xmapsto{f} y & n_3 & \coloneqq t_f \cdot n_2 \\ + \implies & n_4 \Vdash y' \xmapsto{f\circ g} y & n_4 & \coloneqq \langle n_2, n_3 \rangle \\ + \implies & n_5 \Vdash y' \xmapsto{i} y & n_5 & \coloneqq \ell_2 \cdot n_4 \\ + \implies & n_6 \Vdash y' = y & n_6 & \coloneqq n_5 \\ + \implies & n_7 \Vdash x \xmapsto{f} y' & n_7 & \coloneqq r_f \cdot \langle n_3, n_2, s_Y \cdot n_6 \rangle. + \end{align*}$$ + Therefore, if we let $s$ be the encoding of a program representing the transformation from $n$ to $n_7$ in the right column, then $n_s \vdash y_s = y_s$; $s \cdot n_s \downarrow$; and there exists $x\in X$ such that $s \cdot n_s \Vdash x \xmapsto{f} y_s$. This contradicts the choice of $y_s$. + + Therefore, $\Hom(Y', X) \to \Hom(Y', Y)$ is not surjective. Again, $(Y', E_{Y'})$ is isomorphic to an object with $Y' \subseteq \IN$. + + (Also, note that if $(X, E_X)$ is an object with $X \subseteq \IN$, then $(\IN, E_X)$ is also an object which is isomorphic to $(X, E_X)$; therefore, in the generating set, we can in fact require that $X = \IN$.) + unsatisfied_properties: - property: skeletal proof: Consider $(X, \IN \times \Delta_X)$ and $(Y, \IN \times \Delta_Y)$ for bijective but unequal sets $X, Y$. From 8ff10c909f1dd9fe0aa850f5daf5f4f0f3f1df31 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Thu, 10 Sep 2026 17:44:00 -0400 Subject: [PATCH 6/9] Simplify: I forgot that generating sets in a balanced category are automatically extremal --- database/data/categories/Eff.yaml | 22 +++------------------- 1 file changed, 3 insertions(+), 19 deletions(-) diff --git a/database/data/categories/Eff.yaml b/database/data/categories/Eff.yaml index 333ef7eca..5eb403e7d 100644 --- a/database/data/categories/Eff.yaml +++ b/database/data/categories/Eff.yaml @@ -55,9 +55,9 @@ satisfied_properties: - 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: extremal generating set + - property: generating set proof: >- - We claim that the collection of all $(X, E_X)$ with $X \subseteq \IN$ forms an extremal generating set. First, to see it is a generating set, suppose we have two effective functional relations $f, g$ between $(X, E_X)$ and $(Y, E_Y)$ such that $[f] \ne [g]$. Then either a witness $\ell_1$ or a witness $\ell_2$ does not exist; without loss of generality, suppose $\ell_1$ does not exist. That means that for each $\ell \in \IN$, we can find $n_\ell \in \IN$ and $x_\ell \in X$, $y_\ell \in Y$ such that $n_\ell \Vdash x_\ell \xmapsto{f} y_\ell$ but either $\ell \cdot n_\ell \not\downarrow$ or $\ell \cdot n_ell \not\Vdash x_\ell \xmapsto{g} y_\ell$. In either case, make one such choice for each $\ell$, and let $X' \coloneqq \{ x_\ell \mid \ell \in \IN \}$, and $E_{X'} \coloneqq E_X \cap (\IN \times X' \times X')$. We can then check that $E_{X'}$ is an effective PER; $i \coloneqq E_X \cap (\IN \times X' \times X)$ is an effective functional relation inducing a morphism $[i] : (X', E_{X'}) \to (X, E_X)$. + We claim that the collection of all $(X, E_X)$ with $X \subseteq \IN$ forms a generating set. First, to see it is a generating set, suppose we have two effective functional relations $f, g$ between $(X, E_X)$ and $(Y, E_Y)$ such that $[f] \ne [g]$. Then either a witness $\ell_1$ or a witness $\ell_2$ for the equivalence of $f$ and $g$ does not exist; without loss of generality, suppose $\ell_1$ does not exist. That means that for each $\ell \in \IN$, we can find $n_\ell \in \IN$ and $x_\ell \in X$, $y_\ell \in Y$ such that $n_\ell \Vdash x_\ell \xmapsto{f} y_\ell$ but either $\ell \cdot n_\ell \not\downarrow$ or $\ell \cdot n_ell \not\Vdash x_\ell \xmapsto{g} y_\ell$. In either case, make one such choice for each $\ell$, and let $X' \coloneqq \{ x_\ell \mid \ell \in \IN \}$, and $E_{X'} \coloneqq E_X \cap (\IN \times X' \times X')$. We can then check that $E_{X'}$ is an effective PER; $i \coloneqq E_X \cap (\IN \times X' \times X)$ is an effective functional relation inducing a morphism $[i] : (X', E_{X'}) \to (X, E_X)$. We now claim $[f] \circ [i] \ne [g] \circ [i]$. Suppose to the contrary that $f\circ i$ and $g\circ i$ were equivalent, with witnesses $\ell_1$ and $\ell_2$. Then whenever $x' \in X'$, and $n \Vdash x' \xmapsto{f} y$, we have: $$\begin{align*} @@ -65,7 +65,7 @@ satisfied_properties: \implies & n_2 \Vdash x' \xmapsto{i} x' & n_2 & \coloneqq n_1 \\ \implies & n_3 \Vdash x' \xmapsto{f\circ i} y & n_3 & \coloneqq \langle n_2, n \rangle \\ \implies & n_4 \Vdash x' \xmapsto{g\circ i} y & n_4 & \coloneqq \ell_1 \cdot n_3 \\ - \implies \exists x_2\in X, ~ & n_5 \Vdash x' \xmapsto{i} x_2 & n_5 & \coloneqq p_1(n_4) \\ + \implies \exists x_2\in X, ~ & n_5 \Vdash x' \xmapsto{i} x_2, & n_5 & \coloneqq p_1(n_4) \\ & n_6 \Vdash x_2 \xmapsto{g} y & n_6 & \coloneqq p_2(n_4) \\ \implies & n_7 \Vdash x' = x_2 & n_7 & \coloneqq n_5 \\ \implies & n_8 \Vdash x' \xmapsto{g} y & n_8 & \coloneqq r_g \cdot \langle n_6, s_X \cdot n_7, c_f \cdot n \rangle.\end{align*}$$ @@ -73,22 +73,6 @@ satisfied_properties: On the other hand, $(X', E_{X'})$ is isomorphic to an object with $X' \subseteq \IN$ (in fact, structurally isomorphic, not just isomorphic in $\Eff$). - Similarly, to show it is an extremal generating set, suppose we have an effective functional relation $f$ between $(X, E_X)$ and $(Y, E_Y)$ such that $[f]$ is not an isomorphism. By the above, if $[f]$ is not a monomorphism, then we can find $(U, E_U)$ with $U \subseteq \IN$ such that $\Hom(U, X) \to \Hom(U, Y)$ is not injective. Otherwise, since $\Eff$ is balanced, $[f]$ must not be an epimorphism. Using the description of epimorphisms below, we conclude that for each $s \in \IN$, there exists $n_s \in \IN$ and $y_s \in Y$ such that $n_s \Vdash y_s = y_s$, but either $s \cdot n_s \not\downarrow$ or for all $x \in X$, $s \cdot n_s \not\Vdash x \xmapsto{f} y_s$. In either case, make one such choice for each $s$, and let $Y' \coloneqq \{ y_s \mid s \in \IN \}$, $E_{Y'} \coloneqq E_Y \cap (\IN \times Y' \times Y')$, and $i \coloneqq E_Y \cap (\IN \times Y' \times Y)$. Then $E_{Y'}$ is an effective PER, $i$ is an effective functional relation inducing a morphism $[i] : (Y', E_{Y'}) \to (Y, E_Y)$. - - We now claim that the conditions above make it impossible for there to be a functional relation $g$ between $(Y', E_{Y'})$ and $(X, E_X)$ such that $[i] = [f] \circ [g]$, with witnesses $\ell_1$ and $\ell_2$ of the equivalence of $i$ and $f \circ g$. Suppose, to the contrary, we did have such a functional relation $g$. Then whenever $y' \in Y'$ and $n \Vdash y' = y'$, we have: - $$\begin{align*} - \exists x\in X, ~ & n_1 \Vdash y' \xmapsto{g} x & n_1 & \coloneqq t_g \cdot n \\ - \implies & n_2 \Vdash x = x & n_2 & \coloneqq c_g \cdot n_1 \\ - \implies \exists y\in Y, ~ & n_3 \Vdash x \xmapsto{f} y & n_3 & \coloneqq t_f \cdot n_2 \\ - \implies & n_4 \Vdash y' \xmapsto{f\circ g} y & n_4 & \coloneqq \langle n_2, n_3 \rangle \\ - \implies & n_5 \Vdash y' \xmapsto{i} y & n_5 & \coloneqq \ell_2 \cdot n_4 \\ - \implies & n_6 \Vdash y' = y & n_6 & \coloneqq n_5 \\ - \implies & n_7 \Vdash x \xmapsto{f} y' & n_7 & \coloneqq r_f \cdot \langle n_3, n_2, s_Y \cdot n_6 \rangle. - \end{align*}$$ - Therefore, if we let $s$ be the encoding of a program representing the transformation from $n$ to $n_7$ in the right column, then $n_s \vdash y_s = y_s$; $s \cdot n_s \downarrow$; and there exists $x\in X$ such that $s \cdot n_s \Vdash x \xmapsto{f} y_s$. This contradicts the choice of $y_s$. - - Therefore, $\Hom(Y', X) \to \Hom(Y', Y)$ is not surjective. Again, $(Y', E_{Y'})$ is isomorphic to an object with $Y' \subseteq \IN$. - (Also, note that if $(X, E_X)$ is an object with $X \subseteq \IN$, then $(\IN, E_X)$ is also an object which is isomorphic to $(X, E_X)$; therefore, in the generating set, we can in fact require that $X = \IN$.) unsatisfied_properties: From fcef882dc27c6b8212903b77bd1de1846b156d54 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Fri, 11 Sep 2026 21:42:30 -0400 Subject: [PATCH 7/9] Address some initial review comments --- database/data/categories/Eff.yaml | 12 ++++++------ database/data/config.yaml | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/database/data/categories/Eff.yaml b/database/data/categories/Eff.yaml index 5eb403e7d..029a9e31b 100644 --- a/database/data/categories/Eff.yaml +++ b/database/data/categories/Eff.yaml @@ -6,15 +6,15 @@ morphisms: A morphism $(X, E_X) \to (Y, E_Y)$ is a subset $f \subseteq \IN \time description: >- The effective topos gives a "realizability" model of first-order intuitionistic logic roughly matching the principles of constructive mathematics — for example, that a proof of existence requires a computable function on the inputs whose output is a witness of the property, and similarly that a proof of a disjunction requires a computation (based on inputs from the context) of which branch of the disjunction holds. For instance, in this model, every total function $\IN \to \IN$ is (internally) recursive. Similarly, in the resulting model of constructive analysis, it turns out that every total function $\IR \to \IR$ on the constructive reals is continuous; and the Intermediate Value Theorem fails. - 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$. + 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 \times \IN \xrightarrow{\sim} \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 effective partial equivalence relation if $(p_1)_*(E_X)$ is a partial equivalence relation on $X$ with partial recursive functions relating the corresponding realizers; namely: + 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 effective partial equivalence relation if $(p_{2,3})_*(E_X)$ is a partial equivalence relation on $X$ with partial recursive functions relating the corresponding realizers; namely: * (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$. - Likewise, suppose $f \subseteq \IN \times X \times Y$ where we have fixed effective partial equivalence relations $E_X$ and $E_Y$ on $X$ and $Y$, respectively. We then use notation $n \Vdash x \xmapsto{f} y$ to mean $(n, x, y) \in f$. We will say $f$ is an effective functional relation if $(p_1)_*(f)$ is a functional relation $X / E_X \to Y / E_Y$, with partial recursive functions relating the corresponding realizers; namely: + Likewise, suppose $f \subseteq \IN \times X \times Y$ where we have fixed effective partial equivalence relations $E_X$ and $E_Y$ on $X$ and $Y$, respectively. We then use notation $n \Vdash x \xmapsto{f} y$ to mean $(n, x, y) \in f$. We will say $f$ is an effective functional relation if $(p_{2,3})_*(f)$ is a functional relation $X / E_X \to Y / E_Y$, with partial recursive functions relating the corresponding realizers; namely: * (Domain condition:) There exists $d \in \IN$ such that whenever $n \Vdash x \xmapsto{f} y$, then $d \cdot n \downarrow$ and $d \cdot n \Vdash x = x$. @@ -26,7 +26,7 @@ description: >- * (Totality condition:) There exists $t \in \IN$ such that whenever $n \Vdash x = x$, then $t \cdot n \downarrow$, and there exists $y \in Y$ such that $t \cdot n \Vdash x \xmapsto{f} y$. - Similarly, for two such functional relations $f$ and $g$, we will say $f$ and $g$ are equivalent if $(p_1)_*(f) = (p_1)_*(g)$, with partial recursive functions relating the corresponding realizers; namely: + Similarly, for two such functional relations $f$ and $g$, we will say $f$ and $g$ are equivalent if $(p_{2,3})_*(f) = (p_{2,3})_*(g)$, with partial recursive functions relating the corresponding realizers; namely: * There exists $\ell_1$ such that whenever $n \Vdash x \xmapsto{f} y$, then $\ell_1 \cdot n \downarrow$ and $\ell_1 \cdot n \Vdash x \xmapsto{g} y$. @@ -37,7 +37,7 @@ description: >- nlab_link: https://ncatlab.org/nlab/show/effective+topos tags: - - computation theory + - logic related: - Set @@ -92,7 +92,7 @@ special_objects: initial object: description: $(\varnothing, \varnothing)$ terminal object: - description: $(1, \{ (0, 0, n) \mid n \in \IN \})$ + description: $(1, \{ (n, 0, 0) \mid n \in \IN \})$ coproducts: description: The binary coproduct of $(X, E_X)$ and $(Y, E_Y)$ is $X \sqcup Y$ with the PER given by $\{ (2n, x_1, x_2) \in \IN \times X \times X \mid n \Vdash x_1 = x_2 \} \cup \{ (2n+1, y_1, y_2) \in \IN \times Y \times Y \mid n \Vdash y_1 = y_2 \}$. products: diff --git a/database/data/config.yaml b/database/data/config.yaml index b20576377..a7cfcc460 100644 --- a/database/data/config.yaml +++ b/database/data/config.yaml @@ -4,7 +4,7 @@ structure_tags: - analysis - category theory - combinatorics - - computation theory + - logic - number theory - order theory - set theory From a420bc8b4c2fa9da0044bea08a3bac160fd0fa2e Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Fri, 11 Sep 2026 22:04:52 -0400 Subject: [PATCH 8/9] Add references to proof that power object functor on a topos is monadic --- database/data/category-implications/topos.yaml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/database/data/category-implications/topos.yaml b/database/data/category-implications/topos.yaml index caa5c14ea..a807468f2 100644 --- a/database/data/category-implications/topos.yaml +++ b/database/data/category-implications/topos.yaml @@ -41,7 +41,7 @@ - complete conclusions: - cocomplete - proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' - id: topos_monadic_over_itself_countable_powers assumptions: @@ -49,7 +49,7 @@ - countable powers conclusions: - countable copowers - proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' - id: topos_monadic_over_itself_sequential assumptions: @@ -57,7 +57,7 @@ - sequential limits conclusions: - sequential colimits - proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' - id: topos_monadic_over_itself_sifted assumptions: @@ -65,7 +65,7 @@ - cosifted limits conclusions: - sifted colimits - proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' - id: topos_monadic_over_itself_directed assumptions: @@ -73,7 +73,7 @@ - directed limits conclusions: - directed colimits - proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' - id: topos_monadic_over_itself_filtered assumptions: @@ -81,7 +81,7 @@ - cofiltered limits conclusions: - filtered colimits - proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' - id: topos_monadic_over_itself_aleph1_filtered assumptions: @@ -89,7 +89,7 @@ - ℵ₁-cofiltered limits conclusions: - ℵ₁-filtered colimits - proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' - id: topos_monadic_over_itself_aleph2_powers assumptions: @@ -97,7 +97,7 @@ - ℵ₂-small powers conclusions: - ℵ₂-small copowers - proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' - id: topos_monadic_over_itself_aleph2 assumptions: @@ -105,7 +105,7 @@ - ℵ₂-small products conclusions: - ℵ₂-small coproducts - proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic, and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' + proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' - id: grothendieck_topos_definition assumptions: From 292b5d8597eb379391ba428ad944acb409ea8a29 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Fri, 11 Sep 2026 22:25:30 -0400 Subject: [PATCH 9/9] Add an implication which establishes the effective topos has a cogenerating collection --- database/data/category-implications/topos.yaml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/database/data/category-implications/topos.yaml b/database/data/category-implications/topos.yaml index a807468f2..0da284bd1 100644 --- a/database/data/category-implications/topos.yaml +++ b/database/data/category-implications/topos.yaml @@ -107,6 +107,22 @@ - ℵ₂-small coproducts proof: 'This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).' +- id: topos_generator_implies_cogenerator + assumptions: + - elementary topos + - generator + conclusions: + - cogenerator + proof: 'For an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is right adjoint to $P^{\op} : \T \to \T^{\op}$ and moreover is faithful. The first statement is part of the proof that $P$ is monadic (Johnstone, 2.2.7) and the second is a corollary. Therefore, from Lemma 9 here, if $G$ is a generator of $\T$, then $PG$ is a cogenerator.' + +- id: topos_generating_set_implies_cogenerating_set + assumptions: + - elementary topos + - generating set + conclusions: + - cogenerating set + proof: 'For an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is right adjoint to $P^{\op} : \T \to \T^{\op}$ and moreover is faithful. The first statement is part of the proof that $P$ is monadic (Johnstone, 2.2.7) and the second is a corollary. Therefore, from Lemma 9 here, if $F$ is a generating set of $\T$, then $P_*(F)$ is a cogenerating set.' + - id: grothendieck_topos_definition assumptions: - Grothendieck topos