Abstract and scope
We distinguish three exact correspondences: arbitrary generating presentations versus subobject predicates; partial effective enumerators versus semidecidable predicates; and small higher families versus maps to an object classifier. A Boolean classifier requires extra decidability. A support classifier forgets witnesses. The contribution is a self-contained synthesis with explicit hypotheses and obstructions, not a claim that the standard image, enumeration, or truncation theorems are new.
This is the compact journal-text version. The accompanying full manuscript, manuscript.pdf, supplies the expanded exposition, named propositions, proofs, and bibliography. The supplement includes its LaTeX source, finite checks, and results. This draft makes no claim of independent peer review or machine-checked proof.
1. Conventions
Let $\mathcal E$ be a locally small elementary topos with subobject classifier $\mathrm{true}:1\hookrightarrow\Omega$. Images are stable regular-epimorphism/monomorphism factorizations. No natural numbers object, excluded middle, choice, well-pointedness, or countable coproducts is assumed unless stated. Collections of presentations can be handled in a larger metatheoretic universe.
A generating presentation over $X$ is an arrow $g:A\to X$. A morphism of presentations $g\to h:B\to X$ is $u:A\to B$ with $hu=g$. Write
$$g\sim_X h\iff\operatorname{im}(g)=\operatorname{im}(h),\qquad g\preceq_Xh\iff\operatorname{im}(g)\leq\operatorname{im}(h).$$
Equality here is equality of subobjects, not equality of external supports. Image inclusion need not provide a uniform map of witness objects. A categorical generator in the separate, usual sense is an object $G$ such that $\operatorname{Hom}(G,-)$ is faithful. Such a generator is not identified with $\Omega$: already in sets, $1$ is a generator and $\Omega=2$.
The effective topos $\mathbf{Eff}=\mathbf{RT}(\mathcal K_1)$ is one particular topos. Other realizability toposes depend on their partial combinatory algebra and allowed realizers. We do not treat “computable topos” as an unspecified axiom forcing all predicates to be decidable. See [1–4] for the background constructions.
2. Image semantics
Theorem 1. There are order isomorphisms
$$\operatorname{Gen}_{\mathcal E}(X)/{\sim_X} \cong\operatorname{Sub}_{\mathcal E}(X) \cong\operatorname{Hom}_{\mathcal E}(X,\Omega).$$
The hom-set carries the order of internal implication. The forward map is
$$g\longmapsto P_g,\qquad P_g(x)\equiv\exists a:A\;(g(a)=x).$$
The inverse sends $p:X\to\Omega$ to the comprehension mono $P_p\hookrightarrow X$ obtained by pulling back true.
Proof. Factor $g$ as $A\twoheadrightarrow I_g\hookrightarrow X$. Its image is unique as a subobject. Every mono is its own image, and two presentations give the same subobject exactly when they are related by $\sim_X$. This proves the first isomorphism, including its order. The second is the universal property of the subobject classifier. Internal existential quantification is interpreted by image, giving the displayed formula. The characteristic map and comprehension operations are inverse by uniqueness. No choice of a witness for each generated element is used.
Theorem 2. Image is a reflector from $\mathcal E/X$ to its full subcategory of monos. It localizes the slice at maps inducing isomorphisms on images.
Proof. For a mono $m:P\hookrightarrow X$, a slice map $g\to m$ is unique if it exists and exists precisely when $I_g\leq P$. This is the adjunction $\operatorname{im}_X\dashv J_X$. Its unit is $A\twoheadrightarrow I_g$ over $X$ and its counit is invertible. Let $W_X$ be the slice maps whose induced image map is invertible. The reflector inverts $W_X$, and all its unit components lie in $W_X$. Any functor $F$ inverting $W_X$ therefore has a natural isomorphism $F\cong FJ_X\operatorname{im}_X$. The fully faithful inclusion and invertible counit give uniqueness of this factorization, including natural transformations. Hence
$$ (\mathcal E/X)[W_X^{-1}]\simeq\operatorname{Sub}_{\mathcal E}(X). $$
This is not an equivalence of the original slice with a poset. The maps $1\to1$ and $\mathbb N\to1$ have the same image but different witness sets. A map in $W_X$ need not itself be epi: $1\to2$ over $1$ is an example in sets.
3. Substitution and composition
Proposition 3. For $f:Y\to X$, pullback preserves image:
$$\operatorname{im}(f^*g)=f^*\operatorname{im}(g),\qquad P_{f^*g}=P_g\circ f.$$
Proof. Pull back the image factorization. Both its regular-epi and mono properties are preserved. The characteristic map of a pulled-back mono is the composite characteristic map. Thus Theorem 1 is compatible with substitution as an indexed-poset isomorphism.
Direct image gives $\exists_f\dashv f^*$ on subobject posets, since both sides of
$$\exists_fU\leq V\iff U\leq f^*V$$
assert that $f|_U$ factors through $V$. Pullback stability gives Beck–Chevalley; the two sides of $\exists_f(U\wedge f^*V)=\exists_f(U)\wedge V$ are the image of $U\times_YV\to Y$, proving Frobenius.
If $A\to X\times Y$ and $B\to Y\times Z$ present relations $R,S$, the image of $A\times_YB\to X\times Z$ is
$$T(x,z)\equiv\exists y:Y\;(R(x,y)\wedge S(y,z)).$$
Expanding the two image predicates gives exactly compatible pairs of witnesses. Rebracketing existential conjunction proves associativity at the level of images. Diagonal relations give identities. A particular witness cannot generally be reconstructed from this existential predicate.
If $F:\mathcal E\to\mathcal F$ is a geometric inverse-image functor, it preserves images: it preserves finite limits and, as a left adjoint, coequalizers of kernel pairs. If $\theta:F\Omega_{\mathcal E}\to\Omega_{\mathcal F}$ classifies $F\mathrm{true}$, then
$$\chi_{\operatorname{im}(Fg)}=\theta\circ F(\chi_{\operatorname{im}(g)}).$$
This follows by applying $F$ to the characteristic pullback square. The comparison $\theta$ need not be an isomorphism; arbitrary computational structure is not automatically preserved.
4. Realizability evidence
In a realizability tripos, a predicate on an external index set $I$ is represented by $\varphi(i)\subseteq\mathcal A$. Entailment to $\psi$ requires a single allowed realizer $e$ such that for all $i$ and all $a\in\varphi(i)$, $ea$ is defined and belongs to $\psi(i)$. Pointwise nonemptiness implication is insufficient. No algorithm for enumerating arbitrary $I$ is contained in this description [2–4].
An assembly over $\mathcal K_1$ is a set with nonempty sets of numerical realizers. One partial recursive tracker must transform every input realizer correctly. The standard natural numbers assembly has realizer set $\{n\}$ at $n$.
Example 4. For any external $S\subseteq\mathbb N$, the assembly $(S,n\mapsto\{n\})$ includes into $\mathbb N$ with the identity tracker, and the full embedding of assemblies into $\mathbf{Eff}$ makes it a subobject. Thus it has an $\Omega$-classifier even when $S$ is not computably enumerable. Take the complement of the diagonal halting set.
Example 5. Let $b:\mathbb N\to2$ be an external noncomputable function. Give the underlying set $\mathbb N$ the assembly structure $E_b(n)=\{\langle n,b(n)\rangle\}$. First projection tracks a monomorphism $A_b\to\mathbb N$ whose underlying map is the identity. An inverse would, by fullness of the assembly embedding, have a tracker; its second output coordinate would compute $b$. Thus this is a proper subobject with the same external support as $\mathbb N$. Subobject equality cannot be replaced by support equality.
5. A synthetic effective theorem
Let $j:\Sigma\hookrightarrow\Omega$ be a dominance: true factors through $j$, and the monos classified through $j$ contain identities and are closed under composition. Pullback stability is automatic. Assume also that false factors through $j$ and that all complemented monos are admissible. A partial map $X\rightharpoonup_\Sigma Y$ is a span $X\leftarrow D\to Y$ with admissible monic left leg, modulo isomorphism of spans. This has the familiar partial-map-classifier description
$$\operatorname{Par}_\Sigma(X,Y)\cong\operatorname{Hom}(X,L_\Sigma Y), \qquad L_\Sigma Y=\sum_{p:\Sigma}Y^{[p]}.$$
Here $[p]$ is the truth fiber. In particular $L_\Sigma1\cong\Sigma$. Classification of a partial map and classification of its range are distinct operations [5,6].
Assume a natural numbers object and closure of admissible predicates under existential quantification along $\mathbb N\times Y\to Y$, for every $Y$. We state this separately: individual existence of semidecision structures need not give uniform access to them. The dominance and choice issues are analyzed in [6].
Theorem 6. If $X$ has an admissible diagonal and a specified epimorphism $q:\mathbb N\twoheadrightarrow X$, then
$$\operatorname{Par}_\Sigma(\mathbb N,X)/{\sim_X} \cong\operatorname{Sub}_\Sigma(X) \cong\operatorname{Hom}(X,\Sigma).$$
The relation identifies partial generators exactly when their value maps have equal images; the order is image inclusion. Decidable equality is sufficient for the diagonal hypothesis.
Proof. Write a partial generator as $\mathbb N\xleftarrow{i}D\xrightarrow{v}X$. The graph $D\hookrightarrow D\times X$ of $v$ is a pullback of the admissible diagonal. Its composite with $i\times\mathrm{id}_X$ is an admissible graph mono in $\mathbb N\times X$. Existential closure makes its projected image $\operatorname{im}(v)$ admissible, hence classified by $X\to\Sigma$. Conversely, pull back a given admissible $P\hookrightarrow X$ along $q$. The domain $D\hookrightarrow\mathbb N$ is admissible, and $D\to P$ is epi by pullback stability. The partial generator with value map $D\to P\hookrightarrow X$ therefore has exactly image $P$. This proves surjectivity and, by the stated quotient, injectivity and order preservation.
These are internal semantic constructions. Code extraction additionally requires trackers for the chosen enumeration, equality, and closure operations. The usual semidecidable dominance in $\mathbf{Eff}$ supplies these on the natural numbers. A different realizability model need not mean ordinary Turing computability.
Proposition 7. A subobject's characteristic map factors through $2=1+1\hookrightarrow\Omega$ exactly when the subobject is complemented.
Proof. Pull back the two summands of $2$ to obtain complementary subobjects. Conversely, complementary subobjects $P,Q$ give an isomorphism $P+Q\cong X$ and the required Boolean characteristic map. Enumeration does not supply this complement.
6. Uniform numerical translations
Theorem 8. For $S\subseteq\mathbb N$, the following are equivalent, with effective translations on indices in an acceptable numbering: (a) $S$ is the range of a partial recursive $g:\mathbb N\rightharpoonup\mathbb N$; (b) $S$ is the domain of a partial recursive $c:\mathbb N\rightharpoonup1$; (c) $n\in S$ iff $\exists t\,R(n,t)$ for a total recursive Boolean relation $R$; (d) $S$ is the collection of numerical outputs of a total recursive map $\mathbb N\to\mathbb N+1$, with the extra value interpreted as no output.
Proof. From $g$, recognize $x$ by stages $s=0,1,\ldots$. At stage $s$, simulate each $g(n)$ for $s$ steps for $n\leq s$, accepting if any returns $x$. Each stage is finite, and any real output is eventually found. From $c$, generate $n$ by waiting for $c(n)$ to halt and then returning $n$. Bounded simulation supplies $R$; unbounded search for a successful $t$ recovers $c$. Finally, on paired input $(n,t)$ simulate $g(n)$ for $t$ steps and return either its output or the blank value. Conversely, a partial generator can diverge on the blank outputs of such a total optional-output map. Parameter specialization makes all these translations effective on indices. Their composites preserve ranges, not program text or runtime.
The empty set requires partiality or the blank-output convention. It is not the range of a total $\mathbb N\to\mathbb N$. Every nonempty computably enumerable set does have a total recursive enumeration with repetition: first search for one output, use it as a default, and use paired bounded simulations to enumerate every further output. The nonemptiness assumption makes the initial search terminate. No increasing or injective output schedule is promised.
In the standard semidecidable truth-value representation, a proposition is supplied by a computable bit sequence containing 1 exactly when true. A tracker for $\mathbb N\to\Sigma$ supplies such a sequence uniformly; searching it gives the recognizer. Conversely bounded simulation gives that sequence [4,6].
7. Sharp limitations
Proposition 9. The set $K=\{e\mid\varphi_e(e)\downarrow\}$ is generated and semidecidable but has no total recursive Boolean classifier.
Proof. Direct simulation recognizes it. If a total Boolean $d$ decided it, define a program $r(e)$ to halt exactly when $d(e)=0$ and choose an index $k$ of $r$. Then $k\in K$ iff $r(k)$ halts iff $d(k)=0$ iff $k\notin K$, a contradiction. If both $K$ and its complement were semidecidable, dovetailing the two recognizers would decide $K$; consequently the complement is not computably enumerable.
There is also no algorithm deciding equality of two generators' ranges. Given $e$, let $g_e(n)$ simulate $\varphi_e(e)$ and return 0 only if it halts. Its range equals that of the constant-zero program exactly when $e\in K$. Thus the extensional quotient is not an effective canonicalization. Arbitrary delays and repeated outputs also preclude any runtime equivalence based solely on images.
Proposition 10. A nondegenerate elementary topos with $\mathbb N$ has no epi $q:\mathbb N\twoheadrightarrow\Omega^{\mathbb N}$.
Proof. Define $d(n)=\neg q(n)(n)$. Internal surjectivity yields $\exists k\,(q(k)=d)$. For such $k$, $p=q(k)(k)$ satisfies $p\leftrightarrow\neg p$, which intuitionistically entails false: the forward implication gives $\neg p$, and the reverse then gives $p$. Existential elimination gives a global contradiction. No global witness choice is used. Hence the specified enumeration in Theorem 6 cannot be assumed for every object.
Recovering a section of every image epimorphism would imply that every epi splits. This fails, for example, for the regular action $G\to1$ in the topos of actions of a nontrivial group: a section would be a fixed point. Support likewise loses probabilistic weights: Bernoulli laws of parameters $1/3$ and $2/3$ have identical support classifiers and different distributions.
8. Higher semantics
Let $\mathcal X$ be an infinity-topos. The witness fiber of $g:A\to X$ is
$$F_g(x)=\sum_{a:A}(g(a)=x),\qquad P_g(x)=\left\|F_g(x)\right\|_{-1}.$$
Theorem 11. Slice $(-1)$-truncation reflects $\mathcal X/X$ into its mono objects, computes the image of $g$, commutes with base change, and localizes at morphisms inducing equivalent images.
Proof. For a proposition-valued family $Q$, truncation gives
$$\operatorname{Map}_{/X}(I_g,Q)\simeq\operatorname{Map}_{/X}(A,Q).$$
This is the reflective universal property. Equivalently factor $g$ as an effective epi followed by a mono. Both classes are stable under base change. The unit of reflection preserves images, so any functor inverting all image equivalences factors through reflection, as in Theorem 2. These constructions are standard in [7,8].
The mono subcategory over $X$ is equivalent to a poset, with empty or contractible mapping spaces. Its maximal groupoid of objects is classified by $\operatorname{Map}(X,\Omega)$. Inclusion order is additional structure, not the mapping space itself. In spaces, $S^1\to1$ and $1\to1$ have the same support but different fibers, as their fundamental groups show. Thus support classification forgets genuine higher information.
A size-bounded object classifier yields the stronger correspondence
$$ (\mathcal X_{/X}^{\kappa\text{-small}})^{\simeq} \simeq\operatorname{Map}_{\mathcal X}(X,U_\kappa), $$
for a class of small maps classified by $\widetilde U_\kappa\to U_\kappa$. Sufficiently large regular cardinal bounds supply such classifiers in an infinity-topos [7, Section 6.1.6]. The left side is the maximal infinity-groupoid of families and their equivalences, not the entire slice. Pulling back the universal family recovers the witnesses up to equivalence; applying propositional truncation afterwards gives support. No classifier for all maps of all sizes is asserted. No effective infinity-topos or univalent realization of every ordinary effective topos is constructed here.
9. Verification, responsibility, and contribution
The general equivalence is presentations modulo image equality versus predicates. The effective equivalence is partial computable enumeration versus semidecision, under stated hypotheses. Boolean decision and full higher-family reconstruction require additional structure.
The accompanying Python script passed 42,782 finite cases: image reflection and classification, substitution, existential adjunction and Frobenius, relational identities and associativity, witness composition, and bounded operational translations. Finite sets have sizes 0 through 3; relations use a two-element set; machine tables have explicit halting ticks and finite input supports. These checks do not prove arbitrary-topos claims, decide general nontermination, or constitute kernel verification. The full manuscript distinguishes mathematical proofs from this executable evidence.
Prepared with OpenAI ChatGPT/Codex assistance for an anonymous human submitter. Automation assisted drafting, mathematical checking, references, typesetting, and finite tests. The submitting human remains responsible for review and any submission. No independent referee report or acceptance is claimed.
References
1. S. Mac Lane and I. Moerdijk, Sheaves in Geometry and Logic, Springer, 1992; corrected reprint 1994. Publisher. 2. J. M. E. Hyland, “The effective topos,” in The L. E. J. Brouwer Centenary Symposium, 1982, pp. 165–216. Author-hosted text. 3. J. van Oosten, Realizability: An Introduction to its Categorical Side, Studies in Logic 152, Elsevier, 2008. Publisher. 4. A. Bauer, Notes on realizability, draft 21 February 2025, Sections 3.2 and 4.8. Author-hosted notes. 5. W. Phoa, Domain Theory in Realizability Toposes, PhD thesis 1990; revised LFCS report ECS-LFCS-91-171, 1991. Institutional record. 6. C. Knapp, Partial Functions and Recursion in Univalent Type Theory, PhD thesis, 2020, Chapters 5 and 9. arXiv:2011.00272. 7. J. Lurie, Higher Topos Theory, Princeton, 2009, Sections 5.5.6, 6.1.6, 6.2.3. Author-hosted text. 8. The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, 2013. Official book; arXiv:1308.0729.