Latest papers

20 papers1 paper in the last four weeks, with none the four weeks before. 0.0% of all new papers.

Oct 1, 2026

PRISM: A Category-Theoretic Framework for Measuring and Refining Multimodal Analogies

Analogical reasoning involves identifying and preserving relational structures across domains. However, existing approaches to AI-driven multimodal analogy generation lack an interpretable measure of whether this structure is understood and maintained in the generated output. We address this gap with Pullback Refinement via Interpretable Structural Mapping (PRISM), a modality-agnostic framework for measuring and improving relational alignment in multimodal analogies, evaluated on visual metaphor generation. PRISM represents analogies as explicit relational mappings grounded in category theory and uses VLMs to instantiate these structures across modalities. Its first component, the pullback score, quantifies relational alignment from the resulting graph representation. On the AnaloBench benchmark, selecting the correct analogy purely by pullback score achieves 82.5% accuracy, demonstrating that the score captures meaningful relational information. PRISM's second component is an iterative refinement loop that uses the pullback score as an in-context feedback signal to iteratively revise the generated image towards greater relational depth. VLM-as-a-judge and human evaluations show that PRISM consistently improves metaphor consistency and analogy appropriateness over zero- shot generation, with human participants preferring the refined output in 57.65% of pairwise comparisons. However, a qualitative analysis reveals that refinement can favour visually crowded compositions rather than genuinely deeper relational correspondences.
Aug 19, 2026

Categorical AI phenomenology: A first-person approach

This paper develops a phenomenology-first approach to artificial consciousness by reframing consciousness as the subjective experience enacted through an agent's interface with the world. We shift the methodological focus to first-person structures, modeled mathematically by categories derived from Q-networks to capture actions and phenomenological invariants. In this framework, Q-networks are conceptualized as relational interfaces encoding agent-world interaction, analogous to how the dynamical states of a computer depend on its sensory inputs, previous states, and actions. Our work provides a rigorous framework for interface consciousness to describe computational systems that embed information-processing into phenomenological structure. The approach aligns with 4E approaches to cognition by emphasizing enactive, embedded, and extended dimensions of experience. The paper thus offers a principled, relational, and phenomenological account of artificial phenomenology grounded in categorical mathematics.
Aug 4, 2026

To Describe or Construct Statistical Learning Models Using the Category-theoretical Language

Statistical learning is a fascinating field that has long been the mainstream of machine learning/artificial intelligence. A large number of results have been produced which can be widely applied to real-world problems. It also leads to many research topics and also stimulates new research. This report summarizes some classical statistical learning models and well-known algorithms, especially for amateurs, and provides a category-theoretic perspective on understanding statistical learning models. The aim is to attract researchers from other fields, including basic mathematics, to participate in the research related to statistical learning.
Jul 17, 2026

A cubical formalisation of topos causal models: intervention, forcing, and a contextuality obstruction

Topos causal models recast causal inference inside a topos: a causal world is a presheaf, an intervention is a sub-model named by a characteristic map into the subobject classifier \Om\Om, and reasoning is Kripke-Joyal forcing in an intuitionistic internal language. We give the first axiom-free machine-checked account of this 1-topos core, in Cubical Agda over a previously verified probability monad and do-calculus; the framework is otherwise developed on paper, with central claims stated rather than proved. Three of our results go beyond faithful transcription. We exhibit a contextuality obstruction the programme does not treat: pairwise-consistent local causal data with no global model, detected by a degree-one holonomy class. We delimit the claim that interventions are modelled by the subobject classifier: an intervention and an observation name the same subobject, so \Om\Om fixes the target of a do-operation but not the operation itself, which is surgery on the kernels --- where, on a confounder, the interventional and observational laws differ. And we settle the modal unit --- inflationarity is derivable from j⊤=⊤j\top = \top and naturality, not a fourth axiom. We also machine-check the classifier of sieves with its classification theorem, the pullback collating local mechanisms, and the Kripke-Joyal forcing clauses. The development assumes no axioms and typechecks under Agda's --safe flag, with the ordered field discharged at Q\mathbb{Q}; type-level sheafification and a directed do-calculus are future work.
Jul 16, 2026

Learning in Infinitesimal Non-Compositional Sketches

This paper develops a categorical framework -- Learning in Infinitesimal Non-Compositional Sketches (LINCS) -- as the repair of non-compositionality: failures of diagrams to factor through quotient sketches lifted to the tangent category setting. Machine learning problems are specified as sketches: graphs with commutativity conditions D\mathcal D, limit cones L\mathcal L, and colimit cocones K\mathcal K, generalizing the usual scalarization of loss functions or vector space assumptions. Non-compositionality is defined purely as failure of a universal factorization problem, not as arithmetic error between the desired and actual predictions. Given a learning sketch S=(S,D,L,K)\mathbb S=(S,\mathcal D,\mathcal L,\mathcal K), whose underlying graph is SS, and a model D:J→CD:J \rightarrow C, the base defect is the obstruction to factorization \mboxObs(\mboxFactS(D))\mbox{Obs}(\mbox{Fact}_{\mathbb S}(D)). The tangent lift applies the tangent functor TT to obtain TD:J→CTD:J \rightarrow C, and LINCS is defined as the obstruction \mboxObs(\mboxFactS(TD))\mbox{Obs}(\mbox{Fact}_{\mathbb S}(TD)) -- asking whether infinitesimal perturbations preserve the compositionality constraints.The paper also introduces Tangent Learning Sketches, which are sketches equipped with Cockett-Cruttwell tangent structure. The paper defines the INC endofunctor, which iterates the tangent lift, producing a tower D,TD,T2D,⋯D,TD,T^2D, \cdots of factorization problems. ML is thereby formulated as the search for a coalgebraic fixed point where successive tangent unfoldings stabilize (νT\mboxINCνT_{\mbox{INC}}). Using the Aczel--Mendler theorem, we prove existence of a final INC coalgebra whenever T\mboxINCT_{\mbox{INC}} admits a set-based class realization that creates its final carrier. A detailed experimental evaluation of LINCS is underway in a number of concrete ML settings, including deep learning, large language models, and reinforcement learning, and is described in companion papers.
Jun 30, 2026

A Category Theory Account of AI Identity

Artificial intelligence (AI) systems are routinely modified after deployment through retraining and changes in their environments. These transformations raise a metaphysical question: under what conditions does an AI system remain the same system over time or across deployments? Earlier work formulates synchronic and diachronic identity propositionally, by relating identity within a fixed AI system type to equality of trustworthiness levels. Such criteria specify when identity statements are true, but leave implicit the structure of the states compared, the transformations connecting them, and the temporal organization of persistence. We develop a category-theoretic formalization of AI identity. An AI system type is specified by a datum consisting of a techno-function, a trustworthiness profile, and a trustworthiness-level function. Profile-relative states are connected by admissible lifecycle paths, which are restricted to trustworthiness-level-preserving transformations and quotiented to obtain a reachability category. Temporally admissible functors represent AI system histories, while time-synchronous natural transformations compare realized histories. The formalization yields two categorical interpretations of the earlier AI identity criteria. A weak interpretation recovers identity as equality of trustworthiness level. A strong interpretation requires mutual trustworthiness-preserving reachability, expressed through state isomorphism or natural isomorphism of realized histories. Category theory therefore replaces a single AI identity relation with a structured hierarchy of diachronic and synchronic criteria. The resulting framework identifies identity-related preconditions for transferring responsible-AI claims, evidence, and governance procedures across versions or deployments, without treating categorical identity as sufficient by itself for such transfer.
Jun 27, 2026

Compositional Dynamics in Learning and Mechanics

We give a single compositional setting in which gradient-based learning and Hamiltonian-style mechanics appear as functorial semantics. The syntax is an operad Arr whose objects are input-output interfaces (pairs of manifolds) and whose morphisms are smooth adaptive arrangements, which consist of a reactive parameter space, a lens given by smooth output and input maps, and a real-valued potential. The main technical result of the paper is what we call lens internalization, a lax symmetric monoidal functor Lens(C) →\to C associated to any symmetric monoidal closed category C. Using it, we provide two functors ΦphaseΦ_\text{phase}, ΦconfΦ_\text{conf}: Arr →\to PC into the 2-category of polynomial coalgebras -- input-output discrete dynamical systems -- which we take as the semantics category. ΦphaseΦ_\text{phase} stores both position and momentum, whereas ΦconfΦ_\text{conf} stores only position. When applied to a parameterized function, ΦconfΦ_\text{conf} recovers the gradient descent training algorithm, with backpropagation as the lens' backward pass. When applied to harmonic particles wired together -- in series, or according to any finite directed graph -- one diagram yields two different regimes, both of which are governed by the graph Laplacian: ΦphaseΦ_\text{phase} gives the discrete wave equation, which is conservative and second-order, and ΦconfΦ_\text{conf} gives the discrete heat equation, which is dissipative and first-order. They are two semantics of one adaptive arrangement, e.g. with the same potential in each case. And because Arr is an operad, such diagrams nest -- larger systems wired from smaller ones -- and each semantics assembles a system's dynamics functorially from its parts. These dynamics are moreover executable: a parameterized neural network and a graph of particles both compile, by the same construction, to explicit state machines one can run.
Jun 23, 2026

Infinitesimal Causality

This paper introduces a categorical account of infinitesimal causality in Frobenius Markov categories equipped with tangent-bundle semantics. IDC captures the infinitesimal layer in which interventions act as tangent deformations of copy/discard structure. Two distinct Frobenius structures interact: (1) the categorical Frobenius algebra on classical variables encoding copying, comparing, and discarding; and (2) the geometric Frobenius integrability condition, namely involutive closure of the intervention distribution, distinct from the algebraic Frobenius structure. Categorical causal sufficiency is defined as the compatibility of these two notions. A key observation is that, for structural causal models, infinitesimal causality is most naturally formulated in the slice of deterministic mechanisms over exogenous variables, with visible stochastic kernels obtained only after pushforward. Interventions are tangent vectors that deform the Frobenius copy/discard operations; their Lie brackets measure whether this deformation preserves classical information-flow structure. Pearl's do-calculus is used as a guiding example of intervention identities: ignoring irrelevant interventions corresponds to counit invariance, action/observation exchange to coproduct compatibility with pushforward, and independence to involutive bracket closure of the visible intervention distribution.
Jun 17, 2026

A Categorial and Sheaf-Theoretic Semantics for Autonomic Component Ensembles

The proliferation of large-scale, decentralized systems of autonomous agents, such as swarms of robots and networked cyber-physical systems, presents a formidable challenge to traditional formal methods. The Software Component Ensemble Language (SCEL) offers a formal model for such systems, but its operational semantics is not ideal for reasoning about global, structural, and emergent properties. This report proposes a new, multi-layered mathematical model for SCEL using category theory and sheaf theory. We argue that a society of robots described in SCEL can be formally modeled as a sheaf on a topological space, where components are points, ensembles are open sets, and distributed knowledge forms the sheaf's data. In this framework, computational processes like information sharing become equivalent to the sheaf-theoretic operation of "gluing" local data. System failures can then be understood and quantified as topological obstructions, measurable by sheaf cohomology. This approach transforms the verification of a complex distributed system into the analysis of the geometry of a mathematical object, providing deep, structural insights for the design of robust autonomic systems.
May 27, 2026

Comonadic Morphophonology: A Compositional Framework for Context-Dependent Morphological Rules in Finnish

Composing finite-state transducers (FSTs) for context-dependent morphophonological rules -- consonant gradation, vowel harmony, possessive suffix assimilation -- leads to multiplicative state explosion; neural models sidestep the problem but provide no formal account of the rules themselves. We present the first framework where each morphophonological rule is a function from a focused local context to a single output segment -- the type of a local rule familiar from cellular automata -- and where length-changing rules compose as coKleisli arrows of a comonad. Our central contribution is the Writer comonad (DeletionSet x Zipper), a new algebraic construction that restores strict coKleisli compositionality for such rules: each rule is a coKleisli arrow, extend lifts it to a global transformation, and deletions accumulate as a monoid action rather than requiring intermediate materialization. As supporting evidence, thirteen coKleisli arrows provide an alternative formulation expressing the same morphophonological behaviors that Omorfi encodes via 874 continuation classes (67:1 reduction at the rule-representation level), and the same abstraction enables bidirectional morphology -- a MorphGenerator reuses the analysis arrows for generation. On UD Finnish-TDT, the system achieves 83.92% UPOS accuracy with rule-only disambiguation (94.66% with an external suffix tagger), validating the framework as a practical morphological engine.
May 22, 2026

The Cognitive Categorical Transformer: Category-Theoretic Inductive Biases for Language Modeling

The Cognitive Categorical Transformer (CCT) is a 306M-parameter architecture that augments a pretrained GPT-2 Small backbone with cognitively grounded components derived from category theory and several inspirations from cognitive science. Under a matched-step protocol (215,000 optimizer steps, matched data, matched optimizer and schedule) on WikiText-103, CCT reaches 21.27 validation perplexity, compared with 24.19 for an identically fine-tuned GPT-2 Small baseline. The architecture therefore contributes a 2.92 PPL (12% relative) reduction beyond what in-domain fine-tuning alone provides. A retrain-from-scratch ablation that holds GT-Full simplicial message passing bypassed across the entire seven-phase activation schedule reaches 23.72 PPL, localizing 84% of the architectural improvement (2.45 of 2.92 PPL) to GT-Full. We present the first ablation-validated evidence that simplicial message passing improves language-model perplexity at the 306M-parameter scale on WikiText-103. Published GPT-2 Large reaches 22.05 zero-shot PPL on WikiText-103 with 6.2x more parameters than GPT-2 Small; this paper treats that number as an external published reference, not as the architectural benchmark. Three negative results on consistency-style categorical priors (sheaf smoothing, adjunction round-trip, curvature regularization) and the joint structural-prior result for GT-Full and PrecisionWeightedPP together support an empirical pattern termed the structure/consistency distinction, in which categorical priors that add new topology improve language modeling and those that enforce a consistency identity do not.
Apr 29, 2026

A Dynamical Framework for Cognitive Processes Based on Transformations and Semantic Equivalence

This paper proposes a structural and dynamical framework for modeling cognitive processes within a cybernetic perspective. Cognitive states are represented as elements of a state space evolving through an iterative update rule of the form Xt+1=π(F(f(Xt))),X_{t+1} = π\big(F(f(X_t))\big), where ff describes internal transformations, FF represents interpretative mappings, and ππ enforces semantic equivalence. The model is interpreted as a feedback system integrating transformation, observation, and stabilization. A categorical formulation is introduced to capture compositional structure, while the associated dynamics are analyzed through fixed-point arguments and contraction conditions ensuring stability. To demonstrate the operational character of the framework, a computational illustration is provided, together with a qualitative analysis of the induced dynamics. A concrete linguistic application shows how context-dependent interpretation can be modeled as a trajectory toward a stable semantic class. The proposed approach connects dynamical systems, category theory, and cognitive modeling, and provides a unified representation of cognition as a feedback-driven process evolving toward invariant interpretations.
Apr 12, 2026

Working Paper: Towards Schema-based Learning from a Category-Theoretic Perspective

We introduce a hierarchical categorical framework for Schema-Based Learning (SBL) structured across four interconnected levels. At the schema level, a free multicategory SchsynSch_{syn} encodes fundamental schemas and transformations. An implementation functor I\mathcal{I} maps syntactic schemas to representational languages, inducing via the Grothendieck construction the total category SchimplSch_{impl}. Implemented schemas are mapped by a functor ModelModel into the Kleisli category KL(G)\mathbf{KL(G)} of the Giry monad, yielding probabilistic models, while an instances presheaf assigns evaluated instance spaces. A semantic category SchsemSch_{sem}, defined as a full subcategory of KL(G)\mathbf{KL(G)}, provides semantic grounding through an interpretation functor from SchimplSch_{impl}. At the agent level, SchimplSch_{impl} is equipped with a duoidal structure OSch\mathcal{O}_{Sch} supporting schema-based workflows. A left duoidal action on the category MindMind enables workflow execution over mental objects, whose components include mental spaces, predictive models, and a cognitive kernel composed of memory and cognitive modules. Each module is specified by schema-typed interfaces, duoidal workflows, a success condition, and a logical signature. Memory is formalized categorically via memory subsystems, a presheaf DataMData_M, a monoidal operation category OpsMOps_M, and read/write natural transformations. Together with the BodyBody category, Mind defines the embodied SBL agent. At higher levels, SBL is represented as an object of the agent architecture category ArchCatArchCat, enabling comparison with heterogeneous paradigms, while the WorldWorld category models multi-agent and agent-environment interactions. Altogether, the framework forms a weak hierarchical nn-categorical structure linking schema semantics, cognition, embodiment, architectural abstraction, and world-level interaction.
Mar 30, 2026

Working Paper: Towards a Category-theoretic Comparative Framework for Artificial General Intelligence

AGI has become the Holly Grail of AI with the promise of level intelligence and the major Tech companies around the world are investing unprecedented amounts of resources in its pursuit. Yet, there does not exist a single formal definition and only some empirical AGI benchmarking frameworks currently exist. The main purpose of this paper is to develop a general, algebraic and category theoretic framework for describing, comparing and analysing different possible AGI architectures. Thus, this Category theoretic formalization would also allow to compare different possible candidate AGI architectures, such as, RL, Universal AI, Active Inference, CRL, Schema based Learning, etc. It will allow to unambiguously expose their commonalities and differences, and what is even more important, expose areas for future research. From the applied Category theoretic point of view, we take as inspiration Machines in a Category to provide a modern view of AGI Architectures in a Category. More specifically, this first position paper provides, on one hand, a first exercise on RL, Causal RL and SBL Architectures in a Category, and on the other hand, it is a first step on a broader research program that seeks to provide a unified formal foundation for AGI systems, integrating architectural structure, informational organization, agent realization, agent and environment interaction, behavioural development over time, and the empirical evaluation of properties. This framework is also intended to support the definition of architectural properties, both syntactic and informational, as well as semantic properties of agents and their assessment in environments with explicitly characterized features. We claim that Category Theory and AGI will have a very symbiotic relation.
Mar 26, 2026

From Intent to Evidence: A Categorical Approach for Structural Evaluation of Deep Research Agents

Deep Research Agents (DRAs) aim to answer complex questions by searching the web, checking evidence, and synthesizing conclusions across heterogeneous sources. We introduce a category-theoretic framework for evaluating and improving such agents. The framework treats deep research as a structured mapping from user intent to evidence-grounded conclusions, making retrieval traces, cross-source alignment, and final synthesis explicit. Guided by this view, we derive a mechanism-aware benchmark of 296 bilingual questions. The benchmark targets four structural skills central to real research: following multi-hop evidence chains, verifying claims across sources, re-ordering fragmented information, and rejecting unsupported assumptions. We evaluate 16 frontier systems with human verification and find that these structural tasks remain highly challenging: the best system reaches only 19.9% average accuracy. The results show that strong agents can sometimes reorganize evidence and detect false premises, but still struggle with long-horizon synthesis and intersection-heavy verification. Beyond evaluation, the same theory also leads to practical system improvements. We instantiate theory-guided interventions such as tracked search, which preserves retrieval traces, and category tools, which add explicit verification and synthesis steps. These interventions yield measurable gains in API-based deep research systems. Our work therefore provides both a challenging benchmark and concrete design guidance for building more reliable research agents.
Mar 3, 2026

Coalgebras for categorical deep learning: Representability and universal approximation

Categorical deep learning (CDL) has recently emerged as a framework that leverages category theory to unify diverse neural architectures. While geometric deep learning (GDL) is grounded in the specific context of invariants of group actions, CDL aims to provide domain-independent abstractions for reasoning about models and their properties. In this paper, we contribute to this program by developing a coalgebraic foundation for equivariant representation in deep learning, as classical notions of group actions and equivariant maps are naturally generalized by the coalgebraic formalism. Our first main result demonstrates that, given an embedding of data sets formalized as a functor from SET to VECT, and given a notion of invariant behavior on data sets modeled by an endofunctor on SET, there is a corresponding endofunctor on VECT that is compatible with the embedding in the sense that this lifted functor recovers the analogous notion of invariant behavior on the embedded data. Building on this foundation, we then establish a universal approximation theorem for equivariant maps in this generalized setting. We show that continuous equivariant functions can be approximated within our coalgebraic framework for a broad class of symmetries. This work thus provides a categorical bridge between the abstract specification of invariant behavior and its concrete realization in neural architectures.
Mar 2, 2026

The Theory behind UMAP?

In 2018, McInnes et al. introduced a dimensionality reduction algorithm called UMAP, which enjoys wide popularity among data scientists. Their work introduces a finite variant of a functor called the metric realization, based on an unpublished draft by Spivak. This draft contains many errors, most of which are reproduced by McInnes et al. and subsequent publications. This article aims to repair these errors and provide a self-contained document with the full derivation of Spivak's functors and McInnes et al.'s finite variant. We contribute an explicit description of the metric realization and related functors. At the end, we discuss the UMAP algorithm, as well as claims about properties of the algorithm and the correspondence of McInnes et al.'s finite variant to the UMAP algorithm.
Feb 20, 2026

Interactions that reshape the interfaces of the interacting parties

Polynomial functors model systems with interfaces: each polynomial specifies the outputs a system can produce and, for each output, the inputs it accepts. The bicategory Org\mathbb{O}\mathbf{rg} of dynamic organizations \cite{spivak2021learners} gives a notion of state-driven interaction patterns that evolves over time, but each system's interface remains fixed throughout the interaction. Yet in many systems, the outputs sent and inputs received can reshape the interface itself: a cell differentiating in response to chemical signals gains or loses receptors; a sensor damaged by its input loses a channel; a neural network may grow its output resolution during training. Here we introduce polynomial trees, elements of the terminal (u◃u)(u\triangleleft u)-coalgebra where uu is the polynomial associated to a universe of sets, to model such systems: a polynomial tree is a coinductive tree whose nodes carry polynomials, and in which each round of interaction -- an output chosen and an input received -- determines a child tree, hence the next interface. We construct a monoidal closed category PolyTr\mathbf{PolyTr} of polynomial trees, with coinductively-defined morphisms, tensor product, and internal hom. We then build a bicategory OrgTr\mathbb{O}\mathbf{rgTr} generalizing Org\mathbb{O}\mathbf{rg}, whose hom-categories parametrize morphisms by state sets with coinductive action-and-update data. We provide a locally fully faithful functor Org→OrgTr\mathbb{O}\mathbf{rg}\to\mathbb{O}\mathbf{rgTr} via constant trees, those for which the interfaces do not change through time. We illustrate the generalization by suggesting a notion of progressive generative adversarial networks, where gradient feedback determines when the image-generation interface grows to a higher resolution.
Feb 18, 2026

Causal and Compositional Abstraction

Abstracting from a low level to a more explanatory high level of description, and ideally while preserving causal structure, is fundamental to scientific practice, to causal inference problems, and to robust, efficient and interpretable AI. We present a general account of abstractions between low and high level models as natural transformations, focusing on the case of causal models. This provides a new formalisation of causal abstraction, unifying several notions in the literature, including constructive causal abstraction, Q-ττ consistency, abstractions based on interchange interventions, and distributed' causal abstractions. Our approach is formalised in terms of category theory, and uses the general notion of a compositional model with a given set of queries and semantics in a monoidal, cd- or Markov category; causal models and their queries such as interventions being special cases. We identify two basic notions of abstraction: downward abstractions mapping queries from high to low level; and upward abstractions, mapping concrete queries such as Do-interventions from low to high. Although usually presented as the latter, we show how common causal abstractions may, more fundamentally, be understood in terms of the former. Our approach also leads us to consider a new stronger notion of component-level' abstraction, applying to the individual components of a model. In particular, this yields a novel, strengthened form of constructive causal abstraction at the mechanism-level, for which we prove characterisation results. Finally, we show that abstraction can be generalised to further compositional models, including those with a quantum semantics implemented by quantum circuits, and we take first steps in exploring abstractions between quantum compositional circuit models and high-level classical causal models as a means to explainable quantum AI.
May 21, 2025

Unraveling the iterative CHAD

Combinatory Homomorphic Automatic Differentiation (CHAD) was originally formulated as a semantics-driven source-to-source transformation for reverse-mode automatic differentiation of total functional programs. We extend CHAD to programs with partial operations, data-dependent conditionals, and while-loops, preserving its defining principle of structure-preserving semantics. Our main contribution is the introduction of iteration-extensive indexed categories, which integrate iteration into dependently typed programming languages. Iteration in the base category lifts to parameterized initial algebras in the indexed category, yielding fibred iteration on the op-Grothendieck construction. Its total category is the category of containers associated with the dependently typed target language. This framework characterizes iterative CHAD as the unique iterative Freyd category morphism from the source language's syntactic category to the target language's category of containers that maps each primitive operation to its transposed derivative. Using the universal property of the syntactic model, we prove that the transformed programs compute the reverse-mode derivatives of the original programs. The resulting theory connects fixpoint operators in indexed categories with a structure-preserving construction and correctness proof for iterative CHAD.