Towards Grounding AGI's World Models: A Two-Topos, HoTT-Based Epistemic Architecture

Towards Grounding AGI’s World Models: A Two-Topos, HoTT-Based Epistemic Architecture Hironao Nakamura December 2025 Abstract Artificial General Intelligence (AGI) increasingly depends on world models: internal structures that support prediction, abstraction, and long-term planning. Despite the success of large language models and neural world models, we still lack a mathematically clear account of how such structures can be both grounded in raw observations and flexible enough to evolve. Homotopy Type Theory (HoTT) and Univalent Foundations have been proposed as powerful internal languages for AGI, but Potapov and Bogdanov argue that HoTT-based architectures face three major obstacles: grounded types, dynamic type change, and heuristics. This paper argues that these obstacles reflect an architectural mistake rather than a fundamental flaw in HoTT. The mistake is to force observations, concepts, and meta-level dynamics into a single HoTT universe of types. Building on previous work, we instead propose a two-topos epistemic architecture for AGI world models: an observation topos 𝐸obs modeling fields of local observations, a concept topos 𝐸con whose internal logic behaves like HoTT, and a grounding geometric morphism 𝑔 ∶ 𝐸obs → 𝐸con that structurally mediates prediction and abstraction. Within this architecture, groundedness becomes a relation across layers, expressed by monomorphisms Sh(𝐹) ↪ 𝑔∗(𝐴) between observation fields and concepts. Dynamic type change is reinterpreted as theory change at the topos level, via transitions between conceptual toposes, and heuristics appear as meta-level policies over theory/topos and grounding space rather than as ad hoc operations inside HoTT. A minimal 3×3grid world illustrates these ideas in a fully explicit, executable setting. We conclude by outlining a research program that connects the two-topos architecture to neural world models and higher-order probabilistic semantics, positioning it as an epistemic operating system for grounded, adaptive AGI. 1 Introduction Artificial General Intelligence (AGI) research increasingly revolves around world models: internal structures that support prediction, abstraction, long-term planning, and explanation. Despite impressive progress in large-scale neural systems, we still lack a mathematically clear account of how such world models can be both grounded in raw observations and flexible enough to evolve over time. This tension appears in several guises. Large language models (LLMs) exhibit remarkable pattern-matching and few-shot generalization, yet debates about whether they “understand” meaning or merely manipulate form persist. Critiques such as Bender and Koller’s argument that models can climb towards NLU in form but not in grounded semantics highlight an uncomfortable gap between syntactic competence and semantic contact with the world (Bender and Koller 2020). At the same time, work on neural world models—for example, latent-state architectures that learn predictive models of environments (Ha and Schmidhuber 2018; Hafner et al. 2020)—emphasizes the importance of internal structure, but typically stays at the level of engineering heuristics rather than a principled, mathematical account of grounding and theory change. A parallel story has been unfolding in the foundations of mathematics and logic. Homotopy Type Theory (HoTT) and Univalent Foundations provide a powerful internal language for typed, higher-dimensional structure: types behave like spaces, paths act as identifications, and univalence equates isomorphic structures (The Univalent Foundations Program 2013). HoTT has therefore been proposed as a promising candidate for the conceptual core of AGI: a language in which rich concepts, theories, and proofs can live. 1 However, when HoTT is taken not just as an internal language for concepts, but as the single substrate on which an AGI’s entire cognition must run, serious concerns arise. Potapov and Bogdanov, in their paper Univalent Foundations of AGI are (not) All You Need, articulate three major obstacles for HoTT-based AGI (Potapov and Bogdanov 2022): 1. Grounded types. How can raw, noisy sensorimotor streams be represented as HoTT types in a non ad hoc way? What does it mean, structurally, for a type to be grounded in observations? 2. Dynamic type change. Real agents must revise and extend their conceptual repertoire. How can an AGI change its own type universe without incoherence? How can we model theory change when the theory is itself expressed in HoTT? 3. Heuristics. Intelligent behavior depends not only on provable consequences but also on heuristic, exploratory moves—trying a promising conjecture, switching perspectives, or jumping to a different model of the world. How can such meta-level moves be expressed inside a foundational type theory without breaking its logic? These obstacles have been widely interpreted as evidence that “HoTT alone cannot underpin AGI”. HoTT appears too rigid and too pure to accommodate low-level sensory grounding, evolving conceptual systems, and heuristic exploration, at least if we insist that everything—from pixels to proofs—must be encoded as types in a single universe. In this paper, we argue that this diagnosis is only half right. The obstacles are real, but they do not reflect fundamental limitations of HoTT itself. Instead, they reveal an architectural misalignment: an attempt to force observations, concepts, and meta-level dynamics to live in a single layer. HoTT is being asked to do work that naturally belongs to a different mathematical level. Our central claim can be summarized as follows: AGI requires a topos, not a type system. More precisely: •Observations should inhabit a topos-level structure that can express fields of local data, locality, and uncertainty. •Concepts and theories should live in a separate topos whose internal logic behaves like HoTT. • The interaction between them should be expressed by a grounding geometric morphism that structurally mediates prediction and abstraction. Building on previous work, we propose a two-topos, HoTT-based epistemic architecture for AGI world models: • an observation topos 𝐸obs, modeled as a presheaf topos Set𝐶op , where 𝐶is a site of observation points; • a concept topos 𝐸con, whose internal logic behaves like HoTT and serves as the universe of concepts and theories; • a grounding geometric morphism 𝑔 ∶ 𝐸obs → 𝐸con with adjoint pair 𝑔∗⊣ 𝑔∗, encoding top-down prediction and bottom-up abstraction. In a companion paper, Observation is a Topos, Not a Type, we developed this two-layer framework as a mathematical model of observation–concept interaction, introduced design principles for grounding, and explored a minimal grid-world example (Nakamura 2025a). There we treated grounding—how symbols connect to the world in the sense of Harnad’s Symbol Grounding Problem (Harnad 1990)—as the central topic. Here, we treat that framework as the operating system and focus on a specific pain point in the AGI and HoTT communities: Potapov and Bogdanov’s three obstacles. Within the two-topos architecture, we will argue that: 2 •Grounded types are naturally reinterpreted as relations across layers between an observation field 𝐹 ∈ 𝐸obs and a concept 𝐴∈𝐸con such that Sh(𝐹) ↪ 𝑔∗(𝐴). Groundedness is no longer a mysterious property of a single type but a structural alignment between world and concept. •Dynamic type change is re-expressed as theory change at the topos level: moving between conceptual toposes (classifying toposes of different theories) while keeping HoTT as a stable internal logic. The agent changes which topos it uses as its current theory of the world, rather than mutating HoTT itself. •Heuristics become meta-level policies over the space of candidate conceptual toposes and grounding morphisms: strategies for choosing which theory to adopt, which concepts to test, and how to update 𝑔 given new evidence. Logical proof inside HoTT handles structured reasoning within a theory; heuristic policies govern movement between theories and groundings. In this sense, Potapov’s three obstacles are not flaws in HoTT, but symptoms of a one-layer design. Once we separate observations and concepts into distinct toposes linked by a grounding morphism, the obstacles are structurally dissolved: they become natural questions about how to navigate and update a layered architecture, rather than paradoxes inside a single universe of types. This paper is foundational and “towards”-style. We do not present a complete AGI system, nor do we claim empirical validation at human-level scale. Instead, our goals are: • to articulate a clear, mathematically grounded world-model architecture for AGI based on two toposes and HoTT; • to show how this architecture provides structural responses to the three obstacles raised against HoTTbased AGI; • to illustrate the framework on a minimal grid-world example; and • to outline a concrete research program for implementations, probabilistic extensions, and integration with neural world models. The rest of the paper is organized as follows. Section 2 revisits the apparent failure of HoTT for AGI and argues that the root cause is architectural, not logical. Section 3 gives a concise crash course and recap of the two-topos framework, introducing the observation topos 𝐸obs, the concept topos 𝐸con, and the grounding morphism 𝑔. Section 4 is the argumentative core: we structurally reframe Potapov’s three obstacles within the two-topos architecture. Section 5 revisits a finite 3 × 3 grid world to concretize the framework and illustrate how the obstacles look in a toy setting. Section 6 sketches an AGI-scale architecture based on two toposes, including learning, theory change, and heuristic policies over theory space, and connects the proposal to neural world models. Section 7 situates our work within related research on topos theory, HoTT, symbol grounding, conceptual spaces, and LLM-based world models. Section 8 concludes with a summary and a roadmap for future work. 2 Why HoTT Alone Seems to Fail – And Why That Diagnosis Is Misleading 2.1 Symbol grounding and the world-modeling bottleneck The Symbol Grounding Problem, as formulated by Harnad, asks how purely symbolic systems can acquire meanings that are not merely “definitions in terms of other symbols” but are ultimately anchored in sensorimotor experience (Harnad 1990). In modern terms, the question is: When can we say that an internal representation is genuinely about the world, rather than just being a convenient internal token? LLMs and other large models sharpen this question rather than answering it. They demonstrate that vast amounts of ungrounded textual co-occurrence statistics can produce strikingly competent behavior on many tasks. Yet precisely because these models can succeed without any explicit link to non-linguistic reality, they also highlight how far we can go without grounding, and therefore how much is still missing when grounding is required. 3 For AGI, the issue is not only the semantics of individual symbols, but the structure of world models as a whole. An AGI must maintain an internal representation of an environment that: • supports prediction and planning at multiple scales, • can be revised when evidence contradicts current beliefs, • and connects to sensory input and motor output in a non-accidental way. This is a world-modeling bottleneck: we need representations that are flexible and expressive enough to describe complex worlds, yet constrained and structured enough to be learnable and explainable. The Symbol Grounding Problem is not an isolated puzzle but a manifestation of this deeper difficulty. 2.2 HoTT’s apparent limitations for AGI Homotopy Type Theory seems, at first glance, ideally suited for the “top” of an AGI’s world model. It offers: • dependent types for richly structured data, • higher paths for identifications between structures, • univalence to treat isomorphic structures as equal (The Univalent Foundations Program 2013). As an internal language for concepts and theories, HoTT is extremely attractive. Problems arise when we try to make HoTT shoulder the entire burden of cognition, including low-level perception and meta-level control. In particular: 1. Subsymbolic, noisy observation as types. Raw sensorimotor streams—continuous signals, high-dimensional images, event streams—are naturally modeled as fields over space and time with noise and locality. Forcing these directly into HoTT types tends to produce unnatural encodings: • either we discretize and coarsen the data in ad hoc ways, • or we attempt to build enormous type families that mimic metric or probabilistic structure in a fragile way. The result is that “types” are doing double duty as both concepts and raw observation containers, which blurs the distinction between world and theory. 2. Dynamic type change inside a foundational system. Real agents must expand, refine, or even abandon their conceptual schemes. If HoTT is the foundational system, then “changing one’s mind” seems to require: • extending the type universe with new types and constructors, • or redefining existing types. Doing this inside the same formal system risks incoherence or requires sophisticated meta-theory. In practice, we would like a way to talk about moving between theories without tearing up the foundation. 3. Heuristics as internal operations. Intelligent behavior depends on heuristic, exploratory moves: trying a promising conjecture, switching models, or jumping to a simpler theory that “seems to fit” the data. If the only allowed operations are those justified by internal proofs in HoTT, such heuristics have no place. Conversely, if we try to encode heuristics as primitive operations inside the logic, we risk undermining its foundational role. From the perspective of an AGI designer, these obstacles make it look as if “HoTT is too rigid” or “HoTT cannot cope with grounding, change, and heuristics”. It is tempting to conclude that HoTT is simply the wrong tool. 2.3 Structural misplacement: collapsing everything into one layer Our view is that this conclusion is premature, and that the root problem is architectural. In many HoTT-for-AGI proposals, the following design choice—often implicit—is made: Design choice (single-layer HoTT): Represent all of the agent’s internal structure, from raw observations to high-level theories and meta-level heuristics, inside a single HoTT universe of types. 4 Under this design choice: • observations must be encoded as types, • conceptual change must look like internal type redefinition, • and heuristics must appear as operations or principles expressible in the same logic. The three obstacles identified by Potapov and Bogdanov are then almost inevitable: • grounded types become mysterious because we are demanding that types themselves carry sensorimotor content; • dynamic type change becomes dangerous because we are trying to modify the very universe in which our logic lives; • heuristics appear illegitimate because they do not fit the pattern of proof-theoretic reasoning. In other words, HoTT is being asked to play three roles at once: 1. Representation of observations (a low-level, noisy, spatially extended substrate), 2. Representation of concepts and theories (a high-level, structured, logical layer), 3. Representation of meta-level dynamics (policies for changing theories and updating world models). Our central suggestion is that this is simply too much to ask of a single layer. HoTT is extremely well suited to role (2), but much less natural for roles (1) and (3). The obstacles are not signs that HoTT is intrinsically flawed, but that it has been placed at the wrong level of the architecture. 2.4 Potapov’s diagnosis as a symptom list, not a final verdict Seen from this angle, Potapov and Bogdanov’s three obstacles can be read in a different way. We can take their analysis as providing a useful symptom list: • If you insist that observations = types, you will struggle with groundedness. • If you insist that conceptual change = internal mutation of the type universe, you will struggle with dynamic type change. • If you insist that heuristics = internal logical operations, you will struggle to accommodate exploratory behavior. These are real tensions that any HoTT-based AGI designer will encounter under the single-layer design choice. On this we agree. Where we diverge is in the diagnosis. Potapov and Bogdanov conclude that these symptoms show that HoTT “by itself” is not a suitable foundation for AGI (Potapov and Bogdanov 2022). We instead argue that they show the limitations of a particular architectural decision—collapsing observation, concept, and meta-level dynamics into one type-theoretic layer. In the remainder of the paper, we will therefore proceed as follows: • We keep HoTT in the role where it shines: as the internal logic of a conceptual layer, where types are concepts and paths are identifications. • We introduce a separate observation layer, modeled as a topos of fields of observations, where noisy, local, structured data lives. • We express the relation between these layers using a grounding geometric morphism 𝑔, rather than by encoding everything inside HoTT. The rest of the paper shows that, once this layer separation is in place, Potapov’s three obstacles can be naturally reframed and structurally dissolved. The obstacles point to genuine difficulties—but difficulties of a one-layer design, not of HoTT itself. 5 3 Observation is a Topos, Not a Type: The Two-Topos Architecture In this section we give a concise “crash course” on the categorical structures we use, and then recap the two-topos framework developed in the companion paper Observation is a Topos, Not a Type (Nakamura 2025a). Our aim is to convey the intuitive shape of the architecture, not to re-prove any technical results. Full details and proofs can be found in standard references on topos theory and Homotopy Type Theory (Caramello 2017; Lurie 2009; Riehl 2019; The Univalent Foundations Program 2013) and in the companion paper. 3.1 A one-page crash course: presheaves, toposes, and geometric morphisms We begin with three core notions: sites,presheaves, and geometric morphisms. Asite 𝐶is, for our purposes, just a small category that encodes observation points and their relationships. You can think of: • the objects of 𝐶as places where the agent can make local observations (cells in a grid, sensors in a network, positions in a map), • the morphisms of 𝐶as ways of moving information between observation points (adjacency, inclusion, restriction). Apresheaf on 𝐶is a functor 𝐹 ∶ 𝐶op →Set, assigning to each observation point 𝑐 ∈ 𝐶 a set 𝐹(𝑐) of possible local observations, and to each arrow 𝑢 ∶ 𝑐′→ 𝑐 arestriction map 𝐹(𝑢) ∶ 𝐹(𝑐) → 𝐹(𝑐′), that pulls observations back along 𝑢. For example, suppose 𝐶has three sensor locations {𝑐1, 𝑐2, 𝑐3}arranged in a line, with arrows 𝑐1← 𝑐2← 𝑐3 representing adjacency. A simple “color sensor” presheaf can be defined by 𝐹(𝑐𝑖) = {red,green,blue} for each 𝑖, with all restriction maps being the identity. Here 𝐹encodes all possible local color readings the agent might get at each sensor. The category of all presheaves on 𝐶, written 𝐸obs =Set𝐶op , is a standard example of a topos: a category that behaves like a universe of sets, with finite limits, exponentials, and a subobject classifier. Intuitively, a topos is a generalized “world of sets” in which we can do internal logic and mathematics (Caramello 2017; Lurie 2009; Riehl 2019). Presheaves capture locality and structure in observations. However, local data may not always assemble into a coherent global picture. The sheafification Sh(𝐹) of a presheaf 𝐹freely adds the necessary “gluing” conditions so that locally compatible observations yield globally coherent worlds. Informally: Sh(𝐹) is the space of all “ways the world could be,” as seen through the observational structure encoded by 𝐶and 𝐹. Ageometric morphism between toposes 𝑔 ∶ 𝐸 → 𝐹 is, by definition, a pair of adjoint functors 𝑔∗∶ 𝐹 ⇄ 𝐸 ∶ 𝑔∗, 6 where 𝑔∗(the inverse image) preserves finite limits, and 𝑔∗(the direct image) is its right adjoint. Concretely, you can think of a geometric morphism as a structured way of translating between two “worlds of sets.” The functor 𝑔∗pulls objects and structure from 𝐹into 𝐸; the functor 𝑔∗pushes objects and structure from 𝐸 back into 𝐹. In this paper we adopt the following cognitive reading: •𝑔∗corresponds to top-down prediction or concretization: given a concept or theory in the “concept world,” it tells us which observation patterns in the “observation world” are compatible with it. •𝑔∗corresponds to bottom-up abstraction or interpretation: given a field of observations, it tells us which concept or theory in the concept world best summarizes or explains it. We will use these notions at an intuitive and structural level; detailed categorical proofs are not needed to follow the main argument. 3.2 Observation topos 𝐸obs We now specialize to the observation layer. Let 𝐶be a site of observation points: for example, the cells of a grid, the nodes of a graph, or positions in a sensor array. The observation topos is the presheaf topos 𝐸obs =Set𝐶op . An object 𝐹 ∈ 𝐸obs is a field of observations: • for each point 𝑐 ∈ 𝐶, we have a set 𝐹(𝑐) of possible local observations, • for each arrow 𝑢 ∶ 𝑐′→ 𝑐, we have a restriction map 𝐹(𝑢) ∶ 𝐹 (𝑐) → 𝐹(𝑐′)describing how observations transform along the structure of 𝐶. Unlike raw vectors or tensors, presheaves make the relational structure of observations explicit: adjacency, overlap, and restriction all live in 𝐶and are respected by 𝐹. When we pass from 𝐹to its sheafification Sh(𝐹), we obtain the space of globally coherent observation patterns compatible with the local data. In the grid-world example, Sh(𝐹) can be thought of as the set of all colorings of the grid that respect any local constraints imposed by 𝐹. A recurring theme in our broader research program is that many observational domains are not just large but structurally infinite: they can be refined or unfolded without ever reaching a final, reversible stage. In separate work, we formalize this using coalgebras, defining structural infinity as the condition that all transition maps in a coalgebraic unfolding 𝛿𝑛∶ 𝐺𝑛𝑋 → 𝐺𝑛+1𝑋are non-invertible (Nakamura 2025b). Intuitively, continuous sensor fields, analytic refinement, and even homotopical identity towers in HoTT share this non-stabilizing character. This provides a mathematical reason why raw observations fit more naturally in a topos of fields like 𝐸obs than as individual types inside HoTT: they embody an open-ended unfolding that a single, static type system is not meant to contain. 3.3 Concept topos 𝐸con with HoTT-like internal logic On the concept side, we posit a separate topos 𝐸con, whose internal logic behaves like HoTT (The Univalent Foundations Program 2013). Intuitively: • The objects of 𝐸con are concepts and theories. • Its internal types and terms correspond to the usual HoTT notions: –types as spaces or structured entities, –terms as points, –paths as identifications, –univalence equating isomorphic structures. We deliberately do not attempt to encode raw observation data as types in 𝐸con. Instead: 7 • HoTT is used as the internal language of 𝐸con, •𝐸con itself is treated as a conceptual universe, separate from the observational universe 𝐸obs. In this view, the type theory (HoTT) remains stable: logical rules, equality principles, and higher-dimensional structure are fixed. Theory change, rather than being internal mutation of HoTT, will correspond to moving between different conceptual toposes (e.g., different classifying toposes for different theories) while keeping HoTT as the internal logic of each. For the purposes of this paper, we treat 𝐸con at a conceptual level. We assume that it admits an internal logic behaving like HoTT, without committing to a specific (∞, 1)-topos model. Making this connection fully precise—for example, by instantiating 𝐸con as a concrete model of HoTT in the sense of higher topos theory—is an important problem, but it lies beyond the scope of this paper and is left for future work. 3.4 Grounding geometric morphism 𝑔 ∶ 𝐸obs → 𝐸con The two layers are connected by a grounding geometric morphism 𝑔 ∶ 𝐸obs → 𝐸con, equipped with an adjoint pair 𝑔∗∶ 𝐸con ⇄ 𝐸obs ∶ 𝑔∗. We interpret these functors cognitively as follows: •𝑔∗(prediction / concretization): given a concept or theory 𝐴 ∈ 𝐸con, the object 𝑔∗(𝐴) ∈ 𝐸obs represents the space of observational patterns that are compatible with 𝐴. It is the top-down “image” or “expected observation field” induced by 𝐴. •𝑔∗(abstraction / interpretation): given an observation field 𝐹 ∈ 𝐸obs, the object 𝑔∗(𝐹) ∈ 𝐸con represents a conceptual summary or explanation of 𝐹. It is the bottom-up abstraction from raw observations to concepts. The adjunction 𝑔∗⊣ 𝑔∗ encodes the duality between world-to-self and self-to-world directions: • from concept to predicted observation (𝑔∗), • from observation to inferred concept (𝑔∗). In the companion paper, this adjunction is taken as the structural core of grounding (Nakamura 2025a). 3.5 Grounding axioms and the Grounding Representation Principle Not every geometric morphism between toposes is cognitively reasonable. In (Nakamura 2025a), three design principles for a “good” grounding morphism were proposed: 1. Monotonicity. Refinements of observational data (e.g., more precise or more extensive measurements) should be reflected appropriately on the conceptual side. Intuitively: more information should not make the abstraction less informative in an arbitrary way. 2. Sufficiency. If an observation field 𝐹distinguishes certain situations, 𝑔∗(𝐹) should not collapse them inappropriately. The abstraction should preserve distinctions that are semantically relevant. 3. Minimality. Among all concepts 𝐴that can explain an observation 𝐹, the abstraction 𝑔∗(𝐹) should be the coarsest (most abstract) such concept. This suggests an underlying universal property. 8 These are not formal axioms in the sense of a complete axiom system, but design constraints that guide which geometric morphisms qualify as “grounding morphisms.” From these principles emerges the central structural claim of the framework: the Grounding Representation Principle. Grounding Representation Principle. For any observation presheaf 𝐹 ∈ 𝐸obs, there exists a concept type 𝐴𝐹∈ 𝐸con such that Sh(𝐹) ↪ 𝑔∗(𝐴𝐹) as a monomorphism. Here: • Sh(𝐹) is the sheafification of 𝐹, representing the space of globally coherent observation patterns the agent could actually experience. •𝑔∗(𝐴𝐹)is the space of observations permitted by the concept 𝐴𝐹. • The inclusion Sh(𝐹) ↪ 𝑔∗(𝐴𝐹)states that the actual world-as-experienced sits inside the observational affordances of some concept 𝐴𝐹. Intuitively: A concept 𝐴𝐹explains an observation field 𝐹if the observed patterns are among those that the concept “allows”. In a stronger form (left for future work), one can demand that 𝐴𝐹be minimal among all such concepts, echoing the Minimality principle. In the present paper we do not attempt to reprove this principle in full generality. Instead, we: • treat it as part of the operating system of our architecture, • rely on finite-model checks (in the grid world) to illustrate its plausibility, • and focus on how it lets us reframe Potapov’s obstacles in structural terms. 3.6 From recap to reframing We can now restate our earlier slogan more precisely: HoTT becomes powerful once you stop forcing it to carry sensory data. In the two-topos architecture: • observations live in 𝐸obs, • concepts live in 𝐸con, • grounding is expressed by the geometric morphism 𝑔, • and the dual directions 𝑔∗, 𝑔∗capture prediction and abstraction. HoTT is thus freed to play the role of an internal logic of concepts, rather than a universal container for everything. The observation side is handled by topos-theoretic structure tailored to fields and locality. With this layer separation in hand, we are ready to revisit Potapov and Bogdanov’s three obstacles. In the next section we will see how, once observations and concepts are no longer forced into a single HoTT universe, the obstacles change form and can be understood as artifacts of a one-layer design rather than as deep flaws in HoTT itself. 4 Reframing Potapov’s Three Obstacles via Layer Separation We are now in a position to revisit the three obstacles raised by Potapov and Bogdanov against HoTT-based AGI (Potapov and Bogdanov 2022): 1. grounded types, 9 • pick the concept (or set of concepts) that 𝜎satisfies. In the companion paper, concrete implementations of 𝑔∗and 𝑔∗for such concept libraries were given in Python and used to check the Grounding Axioms and the Grounding Representation Principle on samples of grid worlds (Nakamura 2025a). 5.4 Mini-demonstration of the three obstacles dissolving Even in this tiny world, we can see the shape of the three obstacles and how they are reframed. Grounded types Under the single-layer view, we would search for a HoTT type 𝑇grid that “is the grid”, and then try to decide when 𝑇grid is “grounded”. In our two-topos view: • the observation field is 𝐹 ∈ 𝐸obs, • its global sections Sh(𝐹) are the actual colorings, • the concept 𝐴redRegion ∈ 𝐸con represents “there is a connected red region”. If the actual coloring 𝜎exhibits such a region, then 𝜎 ∈ 𝑔∗(𝐴redRegion). More generally, for the observation field 𝐹that yields 𝜎, we have a monomorphism Sh(𝐹) ↪ 𝑔∗(𝐴redRegion), witnessing that the observed world fits inside the space of colorings allowed by the concept. Thus, groundedness appears as a literal inclusion between: • the space of “how the world actually looks” (Sh(𝐹)), • and the space of “how the world can look if concept 𝐴is true” (𝑔∗(𝐴)). Groundedness is no longer a property of an isolated HoTT type; it is a structural relation across the grounding morphism. Dynamic type change Dynamic type change is not very dramatic in a 3×3grid, but we can still illustrate the idea. Suppose the agent starts with a simple conceptual theory 𝑇in which it only considers color counts: • concepts say things like “at least 3 red cells” or “no green cells on the border”, • the corresponding conceptual topos 𝐸𝑇reflects this restricted vocabulary. Over time, the agent notices that some patterns are not captured well by these coarse concepts—for example, whether red cells form a connected shape seems important for predicting rewards, but is invisible to the current theory. The agent then extends its theory to a richer one 𝑇′that includes connectivity-based concepts such as 𝐴redRegion. The new conceptual topos 𝐸𝑇′supports these finer distinctions, and the grounding morphism is updated to 𝑔′∶ 𝐸obs → 𝐸𝑇′. The move 𝐸𝑇→ 𝐸𝑇′is a theory change at the topos level. The internal logic (HoTT) remains the same; what changes is which conceptual topos 𝐸con we use. In this sense, even the tiny grid world can host a toy version of dynamic type change as movement in theory space. Heuristics Finally, heuristics can be seen in a simple policy over a small set of candidate theories. Suppose the agent has two theories: •𝑇counts, which only sees color counts, 16 •𝑇shapes, which also includes connectivity concepts. Let 𝐸counts and 𝐸shapes be the corresponding conceptual topoi with grounding morphisms 𝑔counts and 𝑔shapes. The agent maintains a belief 𝑝(𝑇) over {𝑇counts, 𝑇shapes}. For each new coloring 𝜎, it can: 1. Evaluate how well each theory predicts or compresses 𝜎(e.g., via a simple scoring function). 2. Update 𝑝(𝑇 ) using a Bayesian-like rule. 3. Choose the theory 𝑇⋆with highest expected score to use for the next round of abstraction and planning. This is a heuristic policy over theory space. It is not a proof inside HoTT; it is a meta-level procedure that decides which conceptual topos (and grounding) to adopt. Yet it can be fully formalized in terms of probabilities and scores on a finite set of theories. In the companion paper, a Python implementation (two-layer-topos-hott-framework) performed finite checks of the Grounding Axioms and the Grounding Representation Principle in the grid world (Nakamura 2025a). Extending that code to include a small set of candidate theories and a simple policy over them would yield a concrete, executable demonstration of heuristics in this toy setting. A minimal version of this code will be made available together with the companion paper, so that readers can reproduce the finite checks and experiment with simple theory-selection policies in the grid world. 5.5 From toy example to scalable structure The 3×3grid world is intentionally minimal. It is far from a realistic environment, and we do not claim that it validates the architecture at AGI scale. Its purpose is different: • to show that the two-topos architecture can be instantiated even in the smallest nontrivial worlds, • to demonstrate that the notions of groundedness, theory change, and heuristic policy have clear finitemodel expressions, • and to connect the abstract categorical discussion to code that can actually run. Scalability comes from enriching the site of observations 𝐶: • for images, 𝐶could be a pixel grid or a multi-scale hierarchy of patches; • for sensor arrays, 𝐶could represent sensor locations and their connectivity; • for spatiotemporal data, 𝐶could be a space–time lattice or a more general graph. In each case: •𝐸obs =Set𝐶op represents fields of observations over 𝐶, •𝐸con and HoTT represent structured concepts and theories, • the grounding morphism 𝑔 ∶ 𝐸obs → 𝐸con links them via prediction and abstraction, • and theory/heuristic dynamics operate over the space of conceptual topoi and groundings. The grid world shows, in miniature, how the three obstacles can be reframed and how the two-topos architecture behaves in a fully explicit, finite domain. In the next section, we move beyond the toy example and sketch how this architecture can serve as a world-model “operating system” for AGI. 6 Towards an AGI Architecture Based on Two Toposes The grid world illustrates the two-topos architecture in the smallest possible setting. We now zoom out and sketch how the same ideas can organize an AGI-scale world model. The goal of this section is not to present a complete implementation, but to describe the shape of an architecture that: • separates observations from concepts, • uses HoTT as the internal logic of a conceptual layer, • and treats heuristics and theory change as meta-level dynamics over theories and groundings. 17 6.1 A world-model operating system: 𝐸obs, 𝐸con, 𝑔 At the highest level, we propose to view an AGI’s world model as built on three pillars: 1. Observation layer: a topos 𝐸obs of observation fields. 2. Conceptual layer: a topos 𝐸con whose internal logic behaves like HoTT. 3. Grounding morphism: a geometric morphism 𝑔 ∶ 𝐸obs → 𝐸con, 𝑔∗⊣ 𝑔∗, encoding prediction and abstraction. Concretely: •𝐸obs receives information from: –raw sensors (e.g., cameras, tactile arrays, microphones), – neural encoders that map raw data into structured latent fields (e.g., feature maps, latent state grids), –simulators or learned dynamics models that generate hypothetical observations. •𝐸con hosts: –HoTT-level types representing concepts (e.g., object categories, relations, physical laws), –higher inductive types and path structure capturing identifications and symmetries, –proofs and constructions inside HoTT that encode reasoning and internal derivations. • The grounding morphism 𝑔links them: –𝑔∗(𝐴) tells us what we should see if concept 𝐴is true, –𝑔∗(𝐹) tells us what we should believe conceptually given observation field 𝐹. We can think of this as a world-model operating system (OS): • the observation layer is the “hardware-facing” side, where the AGI meets the world; • the conceptual layer is the “logic-facing” side, where structured reasoning lives; • the grounding morphism is the kernel that mediates between them. 6.2 Learning and conceptual change as movement in theory space An AGI’s conceptual system cannot be static. It must be able to: • refine existing theories, • add new kinds of objects and relations, • sometimes abandon old theories that no longer fit. In our architecture, we model this not as internal mutation of HoTT, but as movement in a space of conceptual toposes. Let us write: •𝑇for a (suitable) theory describing some aspect of the world, •𝐸𝑇for its classifying topos (Caramello 2017), •Th for the (implicit) space of candidate theories. At any time 𝑡, the agent’s current conceptual context is some topos 𝐸(𝑡) con ≅ 𝐸𝑇(𝑡) for a theory 𝑇(𝑡) ∈Th. Learning and conceptual change then involve: • choosing a new theory 𝑇(𝑡+1), • moving from 𝐸𝑇(𝑡) to 𝐸𝑇(𝑡+1) via a geometric morphism Φ𝑡,𝑡+1 ∶ 𝐸𝑇(𝑡) → 𝐸𝑇(𝑡+1) , • updating the grounding morphism to 𝑔(𝑡+1) ∶ 𝐸obs → 𝐸𝑇(𝑡+1) . 18 From this vantage point: •dynamic type change is theory change in topos space, • HoTT remains the internal logic of each 𝐸𝑇, • what varies is which 𝐸𝑇the agent uses as its current model of the world. The grid-world example in Section 5 sketched a tiny version of this: starting with a theory that can only see color counts, then moving to a theory that can express connectivity and shape. At AGI scale, the space Th may be enormous and richly structured, but the idea is the same: Changing concepts is not “mutating the foundation”, but changing which classifying topos we are currently inhabiting. 6.3 Heuristic search as a policy over theories and groundings Because the space of possible theories and groundings is large, an AGI cannot explore it exhaustively. It needs heuristics: • strategies for deciding which theories to try, • rules for when to abandon a failing theory, • and preferences for simplicity, generality, or computational tractability. In the two-topos architecture, such heuristics become policies over the space (𝐸obs, 𝐸con, 𝑔), or more concretely, over candidate pairs (𝑇 , 𝑔𝑇)where: •𝑇is a theory with classifying topos 𝐸𝑇, •𝑔𝑇∶ 𝐸obs → 𝐸𝑇is a grounding morphism compatible with 𝑇. A simple example is the finite Bayesian policy over theories illustrated in Section 4.3: maintain a probability distribution over a finite set of candidate theories, update it based on predictive performance, and choose the theory with highest expected score. More generally, we might consider: • a measurable or topological space of theories Th, • a family of conceptual toposes (𝐸𝑇)𝑇∈Th, • a family of groundings (𝑔𝑇∶ 𝐸obs → 𝐸𝑇)𝑇∈Th, • and a policy 𝜋that, given past observations and performance metrics, selects the next theory 𝑇and grounding 𝑔𝑇to use. Mathematically, such policies can be approached using higher-order probabilistic structure and value functions over transitions in theory space, for example along the lines of categorical models of probability for higher-order computation (Heunen et al. 2017). The key point is conceptual: •HoTT stays where it belongs: as the internal logic of each 𝐸𝑇. •Heuristics live at a higher level: they decide which 𝐸𝑇to use and how to move between them, based on observed data and goals. In this sense, System 2 is “HoTT inside one topos”, while System 1 is “probabilistic, heuristic control over which topos and grounding to deploy”. 6.4 What this paper does, and what remains future work It is important to be clear about the status of the present contribution. This is a foundational, architectural paper. We do not claim to have built or tested a full AGI system. What we do in this paper: • Propose a two-topos, HoTT-based architecture for AGI world models, with: –an observation topos 𝐸obs, –a conceptual topos 𝐸con with HoTT-like internal logic, 19 –and a grounding geometric morphism 𝑔 ∶ 𝐸obs → 𝐸con. • Show how this architecture provides structural responses to three central obstacles for HoTT-based AGI (grounded types, dynamic type change, heuristics), by relocating the problematic aspects to the more natural level of topos and theory space. • Illustrate the framework on a finite 3×3 grid world, connecting the abstract ideas to concrete, executable models and finite verification. What we do not do here (but identify as future work): • Implement a full AGI system using this architecture. • Provide large-scale empirical evaluation on complex environments. • Fully formalize dynamic theory change as paths or higher structure in theory/topos space. • Develop a complete quantitative theory of heuristic policies over (𝐸obs, 𝐸con, 𝑔), including learning of groundings and theories from data. • Extend the framework to detailed models of consciousness, measurement, or value formation (though we see clear avenues for doing so). We see this paper as defining an epistemic operating system and a research program. The subsequent steps—implementations, experiments, and refinements—build on this OS rather than replacing it. A particularly intriguing direction is to study the coalgebraic structure of theory change. In our architecture, an AGI’s conceptual trajectory can be seen as a sequence of conceptual toposes 𝐸(0) con → 𝐸(1) con → 𝐸(2) con → ⋯ arising from repeated updates of theories and groundings. In separate work, we have introduced structural infinity as a coalgebraic characterization of infinite unfolding: a coalgebra (𝑋, 𝛾) is structurally infinite when all transition maps 𝛿𝑛∶ 𝐺𝑛𝑋 → 𝐺𝑛+1𝑋are non-invertible (Nakamura 2025b). Applying this idea here, one could say that an AGI exhibits structurally infinite cognition when its sequence of conceptual toposes never stabilizes—each transition adds genuinely new conceptual structure. Formalizing this connection between structural infinity and epistemic toposes is an open problem and a promising target for future work. 6.5 Connection to neural world models and existing AGI systems Finally, we briefly discuss how the two-topos architecture connects to existing neural world models and AGI-style systems. Architectures such as World Models (Ha and Schmidhuber 2018) and Dreamer (Hafner et al. 2020) learn latent-state models of environments: • an encoder maps observations (e.g., images) into latent states, • a dynamics model predicts future latent states, • a decoder reconstructs observations or rewards, • a controller plans in the latent space. From our perspective, these components can be seen as living at or below the observation topos 𝐸obs: • the site 𝐶may represent spatial, temporal, or feature locations (e.g., pixels, patches, time steps), • presheaves 𝐹 ∶ 𝐶op →Set (or enriched variants) model fields of latent features over 𝐶, • learned dynamics implement maps between such fields. The two-topos architecture does not compete with these methods; rather, it organizes and clarifies their role: • Neural encoders/decoders and dynamics models provide rich, learnable structure for 𝐸obs. • The conceptual topos 𝐸con and HoTT supply a principled language for high-level concepts, theories, and proofs that live above the latent world model. • The grounding morphism 𝑔 ∶ 𝐸obs → 𝐸con tracks how latent fields and high-level concepts are aligned, enabling: 20 –conceptual interpretation of latent states, –top-down conceptual prediction of expected observations, –and coherent updates when predictions fail. In this way, an AGI architecture could combine: • the empirical power of neural world models in capturing complex dynamics, • with the structural clarity of a topos-level observation layer, • and the expressive rigor of HoTT-based conceptual reasoning. The two-topos perspective suggests that future neural-symbolic AGI systems should be designed explicitly as layered architectures: • a rich observation topos with learned structure, • a conceptual topos with HoTT internal logic, • a grounding morphism connecting them, • and heuristic policies governing movement in theory and grounding space. The rest of the paper situates this proposal within related work and reflects on its implications and limitations. 7 Related Work and Discussion The proposal in this paper sits at the intersection of several lines of research: • topos theory and classifying toposes in categorical logic, • Homotopy Type Theory and Univalent Foundations, • the Symbol Grounding Problem and conceptual spaces, • neural world models and LLM-based approaches to AGI. In this section we briefly situate the two-topos architecture within these traditions and highlight points of contact and divergence. 7.1 Topos theory, classifying toposes, and theory change Topos theory originated as a generalization of the category of sets, capable of serving both as a mathematical universe and as a space of generalized models (Lurie 2009; Riehl 2019). Grothendieck toposes, and in particular presheaf toposes, provide a flexible way to model fields of structured data: sheaves and presheaves on a site encode local-to-global behavior in a way that aligns naturally with spatial and relational structure. Our observation topos 𝐸obs =Set𝐶op is a standard presheaf topos. What is novel here is not the topos itself, but its cognitive interpretation as the layer where observation fields live, distinct from the conceptual layer. On the conceptual side, we draw on Caramello’s work on classifying toposes (Caramello 2017). For a theory 𝑇, the classifying topos 𝐸𝑇captures the models of 𝑇in a geometric and logical way. Morphisms of theories 𝑇 → 𝑇 ′induce geometric morphisms 𝐸𝑇→ 𝐸𝑇′. This provides a natural notion of theory change as movement between toposes. Our use of conceptual toposes 𝐸con and theory transitions 𝐸𝑇→ 𝐸𝑇′follows this perspective: we treat an AGI’s conceptual state as “being in” some classifying topos, with dynamic type change modeled as transitions between such toposes. The internal logic of each remains HoTT-like, so we do not need to mutate the foundational logic when we change theories. 7.2 HoTT/UF and its AGI interpretations Homotopy Type Theory (HoTT) and Univalent Foundations (The Univalent Foundations Program 2013) have been proposed as a new foundation for mathematics and as a potential language for formalizing complex structures in computer science. Their appeal for AGI is clear: 21 • types can represent structured data and concepts, • higher paths can represent generalized equalities and symmetries, • univalence aligns the logic with homotopy-theoretic intuition. Several authors have suggested that HoTT could serve as an internal language for AGI or as a foundation for “intensional mathematics” of cognition. Potapov and Bogdanov (Potapov and Bogdanov 2022) make this suggestion explicit, but also argue that HoTT faces three major obstacles when used as the sole internal language of an AGI (grounded types, dynamic type change, heuristics). Our contribution is not to challenge HoTT’s mathematical foundations, but to reposition it: • We treat HoTT as the internal logic of the conceptual topos 𝐸con, • We do not insist that raw observations or heuristic meta-dynamics be encoded as types in the same universe, • We express grounding and dynamics via the two-topos architecture and the grounding morphism 𝑔. In this way, HoTT remains “pure” where it is strong, while the “messy” parts of cognition are handled at the topos level around it. In parallel to the present work, we have also studied the “infinite” side of HoTT and related structures from a coalgebraic perspective. In (Nakamura 2025b), we introduce structural infinity as a unifying notion of infinity across set theory, analysis, continuum refinement, and HoTT: a coalgebra (𝑋, 𝛾) for an endofunctor 𝐺is structurally infinite when all transition maps 𝛿𝑛∶ 𝐺𝑛𝑋 → 𝐺𝑛+1𝑋fail to be isomorphisms. Homotopical infinity in HoTT, such as non-truncated identity towers, arises as one instance of this non-stabilizing unfolding. While the present paper focuses on layer separation for grounding and world models, this coalgebraic view of HoTT’s higher structure complements our architecture and suggests a natural language for describing open-ended conceptual dynamics over theory/topos space. 7.3 Symbol grounding, conceptual spaces, and cognitive structure The Symbol Grounding Problem (Harnad 1990) has inspired a rich variety of approaches: • developmental robotics and sensorimotor coupling, • language games and emergent communication, • geometric representations of concepts. Gärdenfors’ conceptual spaces framework, in particular, models concepts as regions in geometric spaces whose dimensions correspond to quality dimensions (e.g., hue, temperature, weight) (Gärdenfors 2000). Grounding, in this view, is about embedding symbolic structures into such spaces and linking them to perception and action. Our work is compatible with, and in some ways complementary to, conceptual spaces: • The observation topos 𝐸obs can host fields of geometric data (e.g., conceptual-space coordinates over a site 𝐶), • Concepts in 𝐸con can refer to geometric properties (e.g., convex regions, similarity relations), • The grounding morphism 𝑔can mediate between geometric observation fields and higher-level conceptual types. The main difference is that we emphasize logical and categorical structure: • we use toposes and geometric morphisms to describe how observations and concepts are organized, • we use HoTT as a rich internal language for concepts and identifications. Conceptual spaces can be seen as one possible “realization” of parts of 𝐸obs and certain families of concepts in 𝐸con, but our architecture is more general and explicitly layered. 7.4 LLMs, neural world models, and current AGI trends Recent progress in LLMs and neural world models has reshaped the practical landscape of AGI research: 22 • LLMs show that large-scale pattern learning over text (and other modalities) can produce systems with striking fluency and broad competence. • Neural world models, such as World Models (Ha and Schmidhuber 2018) and Dreamer (Hafner et al. 2020), demonstrate that latent-state models can support powerful planning and control. At the same time, critiques like Bender and Koller’s (Bender and Koller 2020) highlight that LLMs, trained only on text, may lack genuine grounding in the world, and that this matters for understanding and robust generalization. World-model approaches address grounding more directly by coupling models to sensory data and control tasks, but typically do so in a predominantly engineering manner: architectures are designed and tuned, but there is little in the way of a unified mathematical story about how the world model, the concepts, and the heuristics fit together. The two-topos architecture can be read as an attempt to provide such a story: • LLMs and neural world models enrich the observation layer 𝐸obs, providing learned structure and dynamics over fields of latent states. • A conceptual topos 𝐸con with HoTT internal logic provides a principled language for higher-level concepts, theories, and proofs, which could be used to analyze and guide model behavior. • The grounding morphism 𝑔 ∶ 𝐸obs → 𝐸con encodes how observations (including latent representations) relate to concepts, making explicit the role that is often implicit in current systems. • Heuristic policies over theory and grounding space provide a structural account of how the system chooses and updates its models, beyond what is captured by gradient descent and RL alone. Our proposal does not claim that existing systems are “wrong”, but that they can be more deeply understood—and potentially improved—by embedding them in a layered, topos-based framework. By making the structure of the world model explicit at the level of toposes and grounding morphisms, the architecture also offers a promising angle for interpretability and safety work, allowing researchers to inspect which concepts are linked to which patterns of observation and how these links evolve over time. 7.5 Comparative summary: grounding, theory change, heuristics To situate our approach more clearly, it is helpful to compare it with a few representative frameworks along four axes: 1. Basic representational object (what do we primarily manipulate?), 2. Treatment of grounding (how do symbols connect to the world?), 3. Handling of theory/type change (how does the system evolve conceptually?), 4. Role of heuristics (where do exploratory, non-deductive moves live?). A schematic comparison might look as follows: Framework Basic object Grounding Theory/type change Heuristics Harnad SGP (Harnad 1990) Symbols + sensorimotor data Grounding via sensorimotor capacities; underspecified mathematically Not central Not central Conceptual spaces (Gärdenfors 2000) Points/regions in geometric spaces Grounding via mapping to quality dimensions Possible via changing spaces/regions Implicit in similarity-based reasoning Potapov & Bogdanov HoTT-AGI (Potapov and Bogdanov 2022) HoTT types “Grounded types” = special HoTT types; problematic “Dynamic type change” inside HoTT Heuristics as internal operations; problematic 23 Framework Basic object Grounding Theory/type change Heuristics Two-topos, HoTT-based architecture (this work) Observation fields (topos) + HoTT concepts Grounding via geometric morphism 𝑔: relations Sh(𝐹) ↪ 𝑔∗(𝐴) Theory change as movement between conceptual toposes Heuristics as policies over theory/topos and grounding space This table is intentionally high-level. The key takeaway is that our approach: • retains the expressive power of HoTT for conceptual structure, • adds a topos-level layer for observations, • and explicitly locates theory change and heuristics at the meta-level of toposes and groundings, rather than inside a single type universe. From this perspective, Potapov’s three obstacles are not so much refuted as reinterpreted: they become constraints on how a layered architecture should be organized, rather than fatal flaws in HoTT. In the next section we conclude by summarizing the proposal and outlining the most promising directions for future work. 8 Conclusion – HoTT Is Not the Problem; The Architecture Was We began with a puzzle that has become increasingly pressing in the AGI era: how can an artificial agent maintain world models that are both grounded in observation and flexible enough to evolve, while supporting rich, structured reasoning? The Symbol Grounding Problem (Harnad 1990), critiques of LLM understanding (Bender and Koller 2020), and the practical successes of neural world models (Ha and Schmidhuber 2018; Hafner et al. 2020) all point to the same bottleneck: we lack a clear mathematical account of how observations, concepts, and meta-level dynamics fit together. Homotopy Type Theory (HoTT) and Univalent Foundations (The Univalent Foundations Program 2013) have been proposed as a powerful internal language for AGI, but Potapov and Bogdanov argue that HoTTbased AGI faces three major obstacles: grounded types, dynamic type change, and heuristics (Potapov and Bogdanov 2022). These have been widely interpreted as evidence that “HoTT alone cannot underpin AGI.” In this paper we argued that this diagnosis is only half right. Our main thesis is that the obstacles are real, but they reflect an architectural misalignment rather than a fundamental flaw in HoTT. When we force observations, concepts, and meta-level updates to live inside a single HoTT universe of types, we should indeed expect trouble. HoTT is being asked to play the role of sensory substrate, conceptual language, and meta-level controller at once. To address this, we proposed a two-topos, HoTT-based world-model architecture: • An observation topos 𝐸obs =Set𝐶op models fields of observations over a site 𝐶, making locality and relational structure explicit. • A conceptual topos 𝐸con has internal logic behaving like HoTT, and serves as the universe of concepts and theories. • A grounding geometric morphism 𝑔 ∶ 𝐸obs → 𝐸con, 𝑔∗⊣ 𝑔∗, structurally mediates between observations and concepts via top-down prediction (𝑔∗) and bottom-up abstraction (𝑔∗). Building on the companion paper Observation is a Topos, Not a Type (Nakamura 2025a), which introduced this framework and established design principles for grounding, we treated the two-topos structure as an epistemic operating system and focused on Potapov and Bogdanov’s three obstacles. Within this architecture, we gave structural responses to each obstacle: 24 •Grounded types. Observations are no longer forced to be HoTT types. Instead, grounding is expressed as a relation across layers. For an observation field 𝐹 ∈ 𝐸obs and a concept 𝐴 ∈ 𝐸con, the Grounding Representation Principle states that, under suitable conditions, there exists a monomorphism Sh(𝐹) ↪ 𝑔∗(𝐴), where Sh(𝐹) is the space of globally coherent observation patterns and 𝑔∗(𝐴) the space of observations permitted by the concept. Groundedness becomes a structural alignment between world and concept via 𝑔, not a mysterious property of a special HoTT type. •Dynamic type change. Rather than mutating the foundational type universe, we model conceptual evolution as theory change at the topos level, following the classifying topos perspective (Caramello 2017). An agent’s conceptual state “lives in” a conceptual topos 𝐸𝑇; changing theories corresponds to moving 𝐸𝑇→ 𝐸𝑇′ between such toposes, while HoTT remains the internal logic of each. Dynamic type change thus becomes movement in theory/topos space, not self-modification of HoTT. •Heuristics. Heuristic, exploratory behavior—choosing which theory to try next, when to abandon a model, how to balance accuracy and simplicity—is expressed as policies over the space of theories and groundings (𝐸obs, 𝐸con, 𝑔). HoTT remains the logic for rigorous reasoning within each conceptual topos; heuristics live at the meta-level, using probabilistic and value-based constructs (as in higher-order probabilistic semantics (Heunen et al. 2017)) to decide which topos and grounding to adopt. In this sense, System 2 is “HoTT inside one topos”, while System 1 is “probabilistic control over which topos and grounding to deploy”. We illustrated these ideas on a minimal 3×3 grid world, where: • observation fields are colorings of the grid in 𝐸obs, • concepts such as “connected red region” live in 𝐸con, • the inclusion Sh(𝐹) ↪ 𝑔∗(𝐴) directly captures when a concept explains an observed coloring, • toy versions of theory change (adding connectivity concepts) and heuristic policies (choosing between coarse and fine theories) can be expressed in finite, executable form. This example is intentionally small, but it shows that the two-topos architecture can be instantiated in fully explicit models and checked with finite verification, as in the companion paper’s Python experiments (Nakamura 2025a). We then sketched how the same architecture could scale to AGI-level systems: • neural encoders, decoders, and latent dynamics populate the observation topos 𝐸obs, • HoTT-based conceptual structure in 𝐸con provides a principled language for high-level concepts and theories, • the grounding morphism 𝑔aligns latent fields with concepts, • and heuristic policies over theory/topos space govern learning and conceptual change. This view does not reject LLMs or neural world models; rather, it categorizes them within a layered picture and suggests how to integrate them with more principled conceptual reasoning. It may be helpful to rephrase our main slogan more precisely: AGI requires a topos, not a type system — more precisely, it requires a topos-level layer for observations and theory contexts, in addition to a powerful internal type theory like HoTT for concepts, and a precise morphism between them. This paper has been deliberately “towards”-style. There are many open questions and limitations: • We have not implemented a full AGI system within this architecture. • We have not provided large-scale empirical validation in complex environments. 25