Research Proposal - Formalizing Traced Monoidal Categories in Agda

Title

Verifiable Foundations for Feedback Structures: Formalising Traced Monoidal Categories in Agda

Introduction

Feedback and recursion are fundamental concepts in programming languages, control systems, and quantum circuits. Traced monoidal categories (TMCs) offer a categorical foundation for modelling such feedback mechanisms. Despite their relevance to fields such as quantum computing and substructural logic, these categories remain under-formalised in modern proof assistants.

In this 42-month PhD project, I will develop a verified formalisation of TMCs in the dependently typed programming language Agda. Building on the work of Hu and Carette [@FormalizingCategoryTheory], I will mechanise the axioms, structure theorems, and advanced constructions associated with TMCs. This work will produce a reusable, verified foundation for feedback structures, supporting applications in AI, quantum computation, and formal semantics.

Background

Basic definitions

A category is an algebraic structure in mathematics that consists of a collection of objects with arrows between them, and an associative composition operator $\circ$; subject to further conditions ommitted here. It has seen much use across a wide array of many disciplines, and is a vibrant ongoing research topic, allowing us to connect disperate topics across the formal sciences.

A functor is an operator that connects categories, acting on the objects and arrows together in a way that preserves structure. A natural transformation is a structure preserving map between functors.

Let $\mathcal{C}$ be a category. An operator $\otimes :\mathcal{C}\times \mathcal{C}\to \mathcal{C}$ is called a monoid if there is a unit object $1$ that associates up to isomorphisms, subject to certain conditions that this isomorphism must satisfy. A monoidal category is simply a category with a suitable monoid structure.

Traced Monoidal Category

We call a monoidal category $\mathcal{C}$ be a left-traced (resp. right-traced) monoidal category, if it is equipped with left (right) trace operator ${\mathrm{tr}}_L^X$ (${\mathrm{tr}}_R^X$), for each object $X$ in $\mathcal{C}$. We call a $\mathcal{C}$ a traced monidal category if it possesses both left and right traces.

Note that every left-traced category with monoidal operator $\otimes$ can be obtained from a right right-traced category with monoidal operator ${\otimes }^{\prime }$ defined such that $A{\otimes }^{\prime }B=B\otimes A$. This means that it suffice to define just ${\mathrm{tr}}_R$.

A right trace

$${\mathrm{tr}}_R^X:\mathcal{C}[A\otimes X,B\otimes X]\Rightarrow \mathcal{C}[A,B]\forall A,B,X:\mathcal{C}$$

is a family of natural transformations from the hom-set $\mathcal{C}[A\otimes X,B\otimes X]$ to $\mathcal{C}[A,B]$ such that the following four axioms listed below hold.

Axioms

A right trace must satisfy the following axioms.

Given $A,B,C,D,X:\mathcal{C}$

Tightening

$$\begin{array}{rlrl}& \text{Given }& & h:A\to B,\\ & & & f:B\otimes X\to C\otimes X,\\ & & & g:C\to D\end{array}$$ $$\begin{array}{r}{\mathrm{tr}}_R^X((g\otimes 1_X)\circ f\circ (h\otimes 1_X))=g\circ {\mathrm{tr}}_R^X(f)\circ h\end{array}$$

This states that if a trace passes through an arrow that does’t interact with the trace, then the scope of the trace can be contracted. [@joyalTracedMonoidalCategories1996]

Sliding

$$\begin{array}{rlrl}& \text{Given }& & f:A\otimes D\to B\otimes C,\\ & & & g:C\to D\end{array}$$ $$\begin{array}{r}{\mathrm{tr}}_R^X((1_B\otimes g)\circ f)={\mathrm{tr}}_R^X(f\circ (1_A\otimes g))\end{array}$$

This ammounts to sliding a function around a functor $g$ around the trace so it ends up occurring before $f$ rather than after. [@joyalTracedMonoidalCategories1996]

Vanishing

$$\begin{array}{rl}\text{Given }& f:A\otimes (C\otimes D)\to B\otimes (C\otimes D),\\ & g:A\otimes 1\to B\otimes 1,\end{array}$$ $$\begin{array}{r}{\mathrm{tr}}_R^{C\otimes D}(f)={\mathrm{tr}}_R^C({\mathrm{tr}}_R^D(f))\\ {\mathrm{tr}}_R^1(f)=f\end{array}$$

The first expresses a kindof currying of traces and the second states that a trace functor over the monoidal identity is the identity. [@joyalTracedMonoidalCategories1996]

Strength

$$\begin{array}{rl}\text{Given }& f:A\otimes X\to B\otimes X\\ & g:C\to D,\end{array}$$ $$\begin{array}{r}{\mathrm{tr}}_R^X(g\otimes f)=g\otimes {\mathrm{tr}}_R^X(f)\end{array}$$

This is similar to tightening but in the other dimension. It expresses that arrows which don’t interact with trace, can be taken out of the scope of the trace. [@joyalTracedMonoidalCategories1996]

Balanced Monoidal categories

A monidal category $\mathcal{C}$ is a braded monoidal category if it has a natural isomorphism $c_{X,Y}:X\otimes Y\Rightarrow Y\otimes X$, called a braid or crossing. These are subject to two hexagon identities spelled out in [@joyalBraidedTensorCategories1993].

A braided monidal category $\mathcal{C}$ is a tortile (or ribbon) monidal category if it has a twist natural isomorphism: ${\theta }_A:A\Rightarrow A$, and is considered balanced if such that ${\theta }_{A\otimes B}=c_{B,A}\circ c_{A,B}\circ ({\theta }_A\otimes {\theta }_B),\forall A,B:\mathcal{C}$ [@joyalGeometryTensorCalculus1991]

A balanced- and traced-monoidal category requires additional two axioms [@joyalTracedMonoidalCategories1996]:

Superimposing

$$\begin{array}{rlrl}& \text{Given }& & f:A\otimes X\to B\otimes X,\\ & & & g:C\to D,\end{array}$$ $$\begin{array}{rl}{\mathrm{tr}}_R^X(f)\otimes g& ={\mathrm{tr}}_R^X((1_B\otimes c_{D,X}^{-1})\circ (f\otimes g)\circ (1_A\otimes c_{C,X}))\\ & ={\mathrm{tr}}_R^X((1_B\otimes c_{D,X})\circ (f\otimes g)\circ (1_A\otimes c_{C,X}^{-1}))\end{array}$$

This is, in effect, states that placing the trace f over top of g without interacting or interlacing them is a reversable action, allowing arrows to pass over top of each-other to move horizontally.

Yanking

$$\begin{array}{rl}{1}_X& ={\mathrm{tr}}_R^X(c_{X,X}\circ ({\theta }^{-1}\otimes 1_X))\\ & ={\mathrm{tr}}_R^X(c_{X,X}^{-1}\circ (\theta \otimes 1_X))\end{array}$$

This provides a way of converting between loops and twists.

Prior Developments

Theoretical Foundations of Traced Monoidal Categories

The formal study of traced monoidal categories (TMCs) originated with Joyal, Street, and Verity’s seminal work, which established the Int construction—a method for embedding TMCs into compact closed categories [@joyalTracedMonoidalCategories1996]. This framework provided a categorical abstraction of feedback loops, unifying diverse applications in linear algebra, knot theory, and programming semantics. Subsequent advances by Hasegawa introduced the uniformity principle, enabling systematic construction of new TMCs from existing ones via full subcategories (e.g., comma categories, coalgebras) [@hasegawaUniformityPrincipleTraced2004]. This principle generalized Plotkin’s fixpoint uniformity to categorical settings, offering tools to propagate traced structures through functorial operations.

Recent breakthroughs by Hu and Vicary recharacterized TMCs as traced pseudomonoids within the bicategory Prof of profunctors [@huTracedMonoidalCategories2021]. Their work externalized TMCs into algebraic structures, enabling graphical reasoning in monoidal bicategories. Key results include equivalence conditions for right $\otimes$-traces and left $\&$¹-traces in $\ast$-autonomous categories and criteria for autonomy [@huFormalizingCategoryTheory2021]. Concurrently, Hasegawa and Lemay advanced the theory of trace-coherent Hopf monads, linking traced monads to symmetric Hopf monads without invoking Eilenberg-Moore categories [@hasegawaTracedMonadsHopf2023]. These developments resolved long-standing questions about monad compatibility but left open challenges in non-Hopf traced monads and autonomy conditions.

Formalization of Monoidal Structures in Proof Assistants

Substantial progress in formalizing category theory has been achieved in Agda, notably through Hu and Carette’s setoid-based, universe-polymorphic library [@huFormalizingCategoryTheory2021]. Their framework supports:

• Proof-relevant hom-setoids with explicit equality transport, avoiding axiom K dependency.
• Monoidal category foundations with closed structures and adjunctions.
• String diagram visualization via ASCII art, though graphical trace operators remain unimplemented.

While this library provides infrastructure for monoidal categories (e.g., naturality proofs, coherence conditions), traced structures are absent. Parallel efforts in Coq’s ViCAR framework developed tactics for rewriting symmetric monoidal diagrams but stopped short of trace operators [@hasegawaUniformityPrincipleTraced2004]. Isabelle/HOL and Lean have basic category theory formalizations but lack monoidal or traced constructs.²

Traced Monads and Algebraic Structures

Lemay’s characterization of traced monads as trace-coherent Hopf monads clarified the relationship between monads and feedback [@hasegawaTracedMonadsHopf2023]. For Cartesian monoidal categories, this connects to Conway operators, while coCartesian settings yield idempotent monads. However, formalizing these results requires reconciling monadic strength with traced axioms, which is a task complicated by universe polymorphism and coherence management.

Gaps and Opportunities

Existing formalizations lack:

1. Trace Axiomatization: No Agda/Coq implementations of Joyal-Street-Verity’s trace axioms (yanking, vanishing). ²

2. Int-Construction: Mechanized proofs of the embedding theorem remain open, critical for applications in quantum semantics [@joyalTracedMonoidalCategories1996] [@hasegawaTracedMonoidalClosed2009b].

3. Hopf Monad Integration: Lemay’s results are yet to be encoded, hindering monad-driven recursion models [@hasegawaTracedMonadsHopf2023].

4. Performance: Setoid-based equality scales poorly for complex traced diagrams, necessitating optimized tactics. [@huFormalizingCategoryTheory2021]

These gaps form the basis for the proposed research, leveraging prior theoretical and formalization work to advance both TMC theory and verified implementations.

Research Programme

This project is structured around three interlinked strands: foundational formalisation, theoretical development, and application-focused integration.

A. Foundational Formalisation in Agda

• Axiomatisation of Traced Monoidal Categories: I will implement the Joyal–Street–Verity axioms [@joyalTracedMonoidalCategories1996] in Agda, extending the existing monoidal framework developed by Hu and Carette [@FormalizingCategoryTheory].
• Braiding and Tortile Structure: I will incorporate braiding and ribbon structures [@reshetikhinRibbonGraphsTheir1990] by adding cross twist operators and verifying the associated coherence laws.
• Universe Polymorphism and Coherence: I will use setoid-based equality [@kinoshitaCategoryTheoreticStructure2014] and universe polymorphism to ensure cross-level compatibility [@FormalizingCategoryTheory].

B. Theoretical Contributions

• Structure Theorem Mechanisation:
  • I will formalise the Int-construction [@joyalTracedMonoidalCategories1996] [@hasegawaTracedMonoidalClosed2009b], a generalisation of the Grothendiek Construction of integers [@grothendieckRevetementsEtalesGroupe1971], as a higher inductive type using definitions compatible with Cubical Agda [@vezzosiCubicalAgdaDependently2021].
  • I will prove formally that every TMC embeds into a compact closed category [@dayNoteCompactClosed1977] [@joyalTracedMonoidalCategories1996].
• Hopf Monad Characterisation:
  • I will mechanise the connection between traced monads and Hopf monads [@bruguieresHopfMonads2007] [@hasegawaRecursionCyclicSharing1997].
• $\ast$-Autonomous Equivalence:
  • I will verify Hu and Vicary’s duality between left $\otimes$-trace and right $\&$¹-trace in $\ast$-autonomous categories [@huTracedMonoidalCategories2021].
• Exploration of Open Problems:
  • I will construct and collect a wide array of examples and counterexamples of various counter examples that satisfy some or all of the braiding, tortile, and trace monoidal axioms to ensure correctness of definitions and applicability across domains.
  • I will formalise conditions under which traced $\ast$-autonomous categories become fully autonomous [@huTracedMonoidalCategories2021] [@PDFQuantumCategories].

C. Applications and Integration

• Quantum Feedback:
  • I will interface with the Quantum IO Monad and implement traced structures for quantum gates and monoidal streams [@dilavoreMonoidalStreamsDataflow2022] [@PDFQuantumCategories] [@greenFormallyVerifiedFunctional2010].
• Recursive Semantics:
  • I will apply TMC formalisation to fixed-point models in substructural logics [@woodFrameworkSubstructuralType2022].
• AI and Systems:
  • I will provide a verified categorical foundation for recursive neural architectures and feedback in AI-enhanced operating systems.

Innovation & Impact

Theoretical Advances

• First full formalisation of the Int-construction [@hasegawaTracedMonoidalClosed2009b].
• Verified treatment of trace in both planar and spherical categorical settings [@huTracedMonoidalCategories2021].
• Formal counterexamples to long-standing conjectures on traced monads may provide new perspectives on monoidal recursion and duality.

Practical Contributions

• Agda Library: I will deliver a reusable, extensible module for any combination of balanced and traced monoidal categories in Agda.
• Tooling for Applied Researchers: The resulting library will support safer reasoning about feedback and recursion in quantum computing, linear logic, and category-theoretic programming.

This work will position Agda as a leading platform for formal category theory and advance the practical verification of high-level mathematical structures in computing.

Timeline & Deliverables

Quarter	Milestone
1–4	Base TMC axiomatisation, compatibility proofs
5–8	Int-construction formalisation, Hopf monad interface
9–12	Quantum feedback case study, performance optimisations
13–16	Non-Hopf monad counterexamples, autonomy conditions
17–20	Recursive semantics integration, documentation
21–24	Final verification, library release, tutorial materials

Anticipated Challenges

1. Universe Management: I will ensure that constructions like the Int-construction remain size-polymorphic and avoid unnecessary universe escalation [@FormalizingCategoryTheory].
2. Equational Reasoning: I will address the difficulty of verifying string diagram equivalences efficiently and ergonomically within Agda, such as by leveraging my professional experience to create a web-based too to translate between string diagrams and Agda equational reasoning.
3. Performance Bottlenecks: I will identify and optimise any performance limitations that arise during automated checking of trace axioms via Agda’s pattern matching.

Conclusion

This project will deliver the first complete mechanisation of traced monoidal categories in any proof assistant, opening the door to formal verification of feedback-driven structures in mathematics and computer science. By integrating verified categorical models with emerging developments in quantum computing and AI systems, I will contribute both theoretical insight and practical infrastructure for future research in high-assurance computing.

---

Citations

Footnotes

1. This should be an upside down ampersand. ↩ ↩²

2. This was concluded from a text search for “Traced Monoidal formalisation source” (without quotes) in the search engine https://duckduckgo.com/, which turned up no relevant source code results or discuss about the formalisation on the first 5 pages. ↩ ↩²