1. Scope, foundations, and contribution
Implementations are objects, implementation changes are arrows, and behavior-preserving changes become equivalences. We choose equality of partial input-output functions as the observation; it forgets running time, memory, and provenance.
We work externally in classical set theory with universes for small categories and presheaves. "Effective" describes program presentations and partial computable denotations. It does not assert computability of all completed objects, semantic tests, or replacements. Countability does not imply recursively enumerable membership.
We specialize established results on universal homotopy theories [1,2], Bousfield localization [3,4], and infinity categories [5,6]. The contribution is the program-edit construction, its semantic separation argument, an endpoint-collapse counterexample, and precise computability obstructions.
This is an external completion. Within realizability, Frumin and van den Berg construct homotopical structures in a full subcategory associated with an elementary topos [9]; van den Berg presents the effective topos as the homotopy category of a path category [10]. Those constructions have separate hypotheses.
2. An effective category of edit histories
Fix an acceptable numbering $(\varphi_e)_{e\in\mathbb N}$ of the unary partial computable functions $\mathbb N\rightharpoonup\mathbb N$, with universal evaluation and the parameterization property. Write
$$ e\equiv_\varphi f \quad\Longleftrightarrow\quad \forall x\;\varphi_e(x)\simeq\varphi_f(x), $$
where Kleene equality means that both sides diverge or both converge to the same value. This is external equality of partial functions, not a decidable test [7,8].
Definition 2.1. Let $\mathcal C$ be the free category on the directed graph with vertices $\mathbb N$ and one generating arrow $u_{e,f}:e\to f$ for every ordered pair. A morphism is a finite vertex sequence
$$ a=(e_0,e_1,\ldots,e_k):e_0\longrightarrow e_k. $$
The length-zero sequence is an identity; composition concatenates at the shared endpoint. A generating loop $u_{e,e}$ records an edit event distinct from the identity. Objects, arrows, source, target, identities, and composition have effective codes, with decidable composability and code equality. Edit syntax asserts no compiler correctness.
Definition 2.2. A generating edit $u_{e,f}$ is safe when $e\equiv_\varphi f$. Let $W_\varphi$ contain precisely those histories for which every generating edit is safe, including all identities.
Lemma 2.3. $W_\varphi$ is a wide subcategory and satisfies two-out-of-three for composable morphisms.
Proof. Safety of a concatenation is equivalent to safety of both constituent histories. Thus identities and composites are safe; if a composite and either constituent are safe, the other constituent is safe. $\square$
We call $(\mathcal C,W_\varphi)$ a relative category of effective program presentations. The category $\mathcal C$ is computably presented; its distinguished subcategory need not be. The raw category has nonidentity endomorphisms at every object, so has no terminal object and is not itself a complete model category.
3. Localization without spurious semantic collapse
Put
$$ \mathcal D_\varphi=N(\mathcal C)[W_\varphi^{-1}]_\infty, \qquad q:N(\mathcal C)\longrightarrow\mathcal D_\varphi. $$
This is localization as an infinity category: functors out of $\mathcal D_\varphi$ correspond to functors out of $N(\mathcal C)$ that carry $W_\varphi$ to equivalences. It exists because the relative category is small [5,6].
Theorem 3.1 (semantic separation). For program indices $e,f$ and a history $a$,
$$ qe\simeq qf\quad\Longleftrightarrow\quad e\equiv_\varphi f, \qquad q(a)\text{ is an equivalence}\quad\Longleftrightarrow\quad a\in W_\varphi. $$
Proof. Let $\mathsf P$ be the set of partial computable functions. Define an ordinary category $\mathcal O$ with objects $\mathsf P$ and
$$ \operatorname{Hom}_{\mathcal O}(b,c)= \begin{cases} \mathbb N,&b=c,\\ \mathbb N_{>0},&b\ne c. \end{cases} $$
Arrows include their endpoints and numerical weight. Composition adds weights; identities have weight zero. This is well-defined because composable weight-zero arrows have equal endpoints. Only weight-zero identities are invertible: nonnegative weights sum to zero only when both vanish.
Define $F:\mathcal C\to\mathcal O$ by $F(e)=\varphi_e$, assigning weight zero to a safe generator and weight one to every other generator. Extend by addition along histories. Every member of $W_\varphi$ maps to an identity, so $F$ factors through $q$ up to equivalence. Equivalent objects of $\mathcal D_\varphi$ therefore have equal images in $\mathcal O$, hence equal partial functions. Conversely, if $e\equiv_\varphi f$, the generator $u_{e,f}$ belongs to $W_\varphi$ and becomes an equivalence. Finally, if $q(a)$ is an equivalence, $F(a)$ is an isomorphism, so has weight zero; every edge of $a$ is safe. The reverse implication is the definition of localization. $\square$
Thus $W_\varphi$ is saturated. The semantic functor $F$ need not be computable.
Remark 3.2 (why endpoints alone fail). Suppose instead that a history were declared weak whenever only its initial and final programs agree extensionally. Choose inequivalent programs $e,f$ and arrows $a:e\to f$, $b:f\to e$. Both $ba$ and $ab$ would then be weak. After localization both composites are invertible, forcing $a$ and $b$ themselves to be invertible. This would identify inequivalent programs. Requiring every elementary edit to be safe prevents this collapse.
4. A model category presenting the theory
Let
$$ \mathsf U=\mathbf{sSet}^{\mathcal C^{op}} $$
carry the projective model structure induced by Kan-Quillen simplicial sets. Weak equivalences and fibrations are objectwise. Generating cofibrations are
$$ y(e)\times\partial\Delta^n\longrightarrow y(e)\times\Delta^n, $$
where $y$ is the discrete simplicial Yoneda embedding. Smallness of $\mathcal C$ gives this cofibrantly generated model structure; its underlying presheaf category is locally presentable. Projective cofibrations are objectwise cofibrations. Since pushouts are objectwise and simplicial sets are left proper, $\mathsf U$ is left proper. It is also simplicial [1,4,5].
Set
$$ S_\varphi=\{y(w)\mid w\in W_\varphi\}, \qquad \mathsf H_\varphi=L_{S_\varphi}\mathsf U. $$
Theorem 4.1 (existence and fibrant objects). $\mathsf H_\varphi$ exists as a left proper combinatorial simplicial model category. Its cofibrations are the projective cofibrations. Its fibrant objects are precisely the objectwise Kan presheaves $X$ such that
$$ X(w):X(f)\longrightarrow X(e) $$
is a weak equivalence whenever $w:e\to f$ lies in $W_\varphi$.
Proof. $S_\varphi$ is a set, even though it is not effectively enumerable. Apply the left proper combinatorial localization theorem [4, Theorem 4.7], with its simplicial version. The representables are projectively cofibrant. For objectwise fibrant $X$, enriched Yoneda identifies the derived mapping space $\operatorname{Map}^{h}(y(e),X)$ with $X(e)$. Thus the locality condition for $y(w)$ is exactly the displayed condition. The remaining assertions are the localization theorem. $\square$
A map $A\to B$ of simplicial presheaves is a weak equivalence in $\mathsf H_\varphi$ exactly when
$$ \operatorname{Map}^{h}_{\mathsf U}(B,X) \longrightarrow\operatorname{Map}^{h}_{\mathsf U}(A,X) $$
is an equivalence for every such local fibrant $X$. This is a mathematical characterization, not a terminating recognition procedure. The identity $\mathsf U\to\mathsf H_\varphi$ is left Quillen. Ordinary localization at these weak equivalences gives its homotopy category; infinity localization retains derived mapping spaces.
5. Identification and universal property
Theorem 5.1 (presheaf identification). There is an equivalence
$$ (\mathsf H_\varphi)_\infty \simeq \mathcal P(\mathcal D_\varphi) =\operatorname{Fun}(\mathcal D_\varphi^{op},\mathcal S). $$
Proof. The projective model presents $\mathcal P(N\mathcal C)$. Under this equivalence its local objects are precisely presheaves taking every arrow of $W_\varphi$ to an equivalence. The universal property of $q$ identifies these, by restriction along $q^{op}$, with all presheaves on $\mathcal D_\varphi$. Restriction is fully faithful. The corresponding reflective subcategory is presented by the left Bousfield localization of Theorem 4.1 [5, Sections 5.5.4 and A.3.7]. $\square$
Write $\mathcal H_\varphi$ for this underlying infinity category and $j(e)=L_{S_\varphi}y(e)$ for its derived representable. The identification sends $j(e)$ to $y_{\mathcal D_\varphi}(qe)$: mapping either object into a presheaf evaluates that presheaf at $qe$. Infinity Yoneda and Theorem 3.1 imply
$$ j(e)\simeq j(f)\quad\Longleftrightarrow\quad\varphi_e=\varphi_f, $$
and
$$ \operatorname{Map}_{\mathcal H_\varphi}(j(e),j(f)) \simeq\operatorname{Map}_{\mathcal D_\varphi}(qe,qf). $$
Thus completion does not introduce extra equivalences between program objects. It does introduce arbitrary presheaves and their homotopy colimits; those are not all effective programs.
Corollary 5.2 (free cocompletion with semantic inversions). For every presentable infinity category $\mathcal E$,
$$ \operatorname{Fun}^{L}(\mathcal H_\varphi,\mathcal E) \simeq \operatorname{Fun}_{W_\varphi}(N\mathcal C,\mathcal E). $$
Proof. Apply the free cocompletion property of presheaves [1,5] and then the defining property of $q$. The superscript $L$ means preservation of small colimits; the subscript on the right means inversion of $W_\varphi$. $\square$
The colimit condition matters: a presentable reflective localization inverts the strongly saturated closure, beyond unrestricted inversion of the original maps.
6. Numberings, compilers, and observation choices
Theorem 6.1 (renumbering invariance). Suppose $\pi:\mathbb N\to\mathbb N$ is a computable bijection between numberings $\varphi,\psi$ with $\psi_{\pi(e)}=\varphi_e$. Then the corresponding relative categories are isomorphic and their localized presheaf model categories are isomorphic as model categories.
Proof. Apply $\pi$ to every vertex of a history. Its computable inverse gives an inverse functor, and denotation preservation identifies the safe histories. Precomposition along this category isomorphism identifies projective structures and their local equivalences. $\square$
Rogers' isomorphism theorem supplies such a permutation between acceptable numberings [7]. This establishes invariance at that precise level, including standard Turing and lambda presentations once they are supplied as acceptable numberings of the same partial functions.
For more general relative categories, relative functors $F,G$ together with natural transformations $GF\Rightarrow\mathrm{id}$ and $FG\Rightarrow\mathrm{id}$ whose components are weak equivalences induce inverse equivalences after infinity localization. Indeed, the transformations become natural equivalences. Their presheaf infinity categories are consequently equivalent. This is a sufficient coherence criterion; mere agreement of translated program outputs does not supply those natural transformations or control the edit-history geometry.
A correct interpreter producing $s(e)$ with $\varphi_{s(e)}=\varphi_e$ gives $j(s(e))\simeq j(e)$. This conclusion is conditional on interpreter correctness. If the observation is enriched to $(\text{output},\text{running time})$, a slow interpreter can fail that condition. The construction works for other chosen observation equivalence relations, but the resulting weak equivalences change.
7. The boundary of effective classification
Theorem 7.1 (recognition obstruction). The relation $e\equiv_\varphi f$ is neither recursively enumerable nor co-recursively enumerable. Consequently there is no algorithm deciding $W_\varphi$-membership, or deciding all weak equivalences between the specified representable arrows in $\mathsf H_\varphi$.
Proof. Let $z$ compute the constant-zero function and let $b$ diverge on every input. Given a machine/input pair $(a,n)$, parameterization effectively produces a program $t(a,n)$ which, on any input, simulates $\varphi_a(n)$ and returns zero if that simulation terminates. Then
$$ t(a,n)\equiv_\varphi z\iff\varphi_a(n)\downarrow, \qquad t(a,n)\equiv_\varphi b\iff\varphi_a(n)\uparrow. $$
If extensional equality were recursively enumerable, the second reduction would enumerate the complement of the halting set. If it were co-recursively enumerable, the first would make the halting set co-recursively enumerable. Both contradict undecidability of halting, since the halting set is recursively enumerable [8].
For a generator $u_{e,f}$, safe membership is exactly extensional equality. By Theorems 3.1 and 5.1, its representable image is a weak equivalence in $\mathsf H_\varphi$ exactly in the same case. Any proposed decision procedure would therefore decide the relation just shown undecidable. $\square$
Corollary 7.2. No uniformly computable invariant with decidable equality completely classifies the equivalence classes of the derived program objects. No recursively enumerable collection of finite certificates can be both sound and complete for all these extensional equalities.
Proof. Comparing the invariant would decide equality. Enumerating all valid certificates and their conclusions would enumerate equality. Both contradict Theorem 7.1. $\square$
These results do not rule out computable cofibrant replacements, structured horn fillers, sound incomplete proof systems, or useful decidable fragments. They rule out complete effective recognition in this particular extensional theory. In particular we have not inferred that every fibrant replacement procedure must itself decide equivalence. Structured effective Kan fibrations address a different constructive question [11].
8. The topos conclusion and its exact meaning
By Theorem 5.1, $\mathcal H_\varphi$ is a presheaf infinity topos. This follows from its identification as $\mathcal P(\mathcal D_\varphi)$, not from an unproved claim that the reflector $\mathcal P(N\mathcal C)\to\mathcal H_\varphi$ is left exact. A presheaf infinity topos admits an intrinsic interpretation of dependent types and higher identity structure, but no realizability or algorithm-extraction principle has thereby been established.
The distinction about left exactness is real. Let $\mathcal A$ be the category $0\to2\leftarrow1$ and invert both nonidentity arrows. Its infinity groupoid completion is contractible, so the local-presheaf category is $\mathcal S$. The reflector sends a span $X_0\leftarrow X_2\to X_1$ to its homotopy pushout. For spans $(*\leftarrow\varnothing\to\varnothing)$ and $(\varnothing\leftarrow\varnothing\to*)$, each reflection is $*$, while their pointwise product reflects to $\varnothing$. Thus this reflector fails to preserve binary products although its target is an infinity topos.
Further accessible left exact localizations of $\mathcal P(\mathcal D_\varphi)$, for example sheafification for a chosen Grothendieck topology, again yield infinity topoi [5, Definition 6.1.0.4]. Arbitrary further Bousfield localizations need not. Hyland's effective topos is an elementary realizability topos; external cocompleteness and presentability cannot simply be assumed for it [9]. No equivalence between it and this presheaf construction is claimed.
9. Reproducibility and limitations
The bundle contains manuscript sources, PDF, and a dependency-free Python checker with a JSON report. Supplied finite labels support checks of bounded histories, category laws, two-out-of-three, the separator, a permutation, and the two counterexamples. A bounded interpreter records timeout as "unknown", never divergence. These finite checks do not prove localization, undecidability, or arbitrary program equality.
The free category retains edit histories. Extra coherence relations, operational observations, or higher rewrite cells are further choices; their invariance is unproved. We have not constructed an internal realizability model, verified compiler, new univalence theorem, or physical reality criterion. The results specify a model category, its infinity presentation, renumbering invariance, and classification boundary.
Authorship and automation. Anonymous submission at the direction of the responsible human researcher. An OpenAI assistant assisted with research, construction, proofs, exposition, and finite checks. The manuscript is not proof-assistant verified. Editorial review and any independent peer review remain separate from these checks.
References
1. D. Dugger. Universal homotopy theories. Advances in Mathematics 164 (2001), 144-176. Author manuscript. 2. D. Dugger. Combinatorial model categories have presentations. Advances in Mathematics 164 (2001), 177-201. Author manuscript. 3. P. S. Hirschhorn. Model Categories and Their Localizations. Mathematical Surveys and Monographs 99, AMS, 2003. Publisher record. 4. C. Barwick. On left and right model categories and left and right Bousfield localizations. Homology, Homotopy and Applications 12(2) (2010), 245-320. Author manuscript, especially Theorem 4.7. 5. J. Lurie. Higher Topos Theory. Annals of Mathematics Studies 170, Princeton University Press, 2009. Author PDF. Sections 5.1.5, 5.5.4, 6.1, A.3.3, A.3.7. 6. E. Riehl. Homotopical categories: from model categories to (infinity,1)-categories. Author manuscript, 2020 version. 7. H. Rogers Jr. Godel numberings of partial recursive functions. Journal of Symbolic Logic 23(3) (1958), 331-341. Publisher record. DOI: 10.2307/2964292. 8. A. M. Turing. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society s2-42 (1936-1937), 230-265. Publisher record. DOI: 10.1112/plms/s2-42.1.230. 9. D. Frumin and B. van den Berg. A homotopy-theoretic model of function extensionality in the effective topos. Mathematical Structures in Computer Science 29(4) (2019), 588-614. Corrected author version. 10. B. van den Berg. Univalent polymorphism. Author manuscript, 2018. 11. B. van den Berg and E. Faber. Effective Kan Fibrations in Simplicial Sets. Springer, 2022. Author manuscript.