Uploaded September 2025 | Updated September 2026, 2 weeks ago
Topos Institute Colloquium, 18th of September 2025.
———
Double categories are a flexible 2-dimensional setting that allows us to encode two types of morphisms between objects, as well as a notion of higher cells. Surprisingly, unlike most categorical structures, there is no canonical notion of “equivalence of double categories”, as it seems that every possible definition requires us to make a choice. In this talk we will illustrate the issue that arises when defining double-categorical equivalences. Then, we will show how we can use homotopy theory to give a decisive answer as to who the “canonical double categorical equivalences” should be: the gregarious equivalences introduced by Campbell. In the process, we will show how to construct a plethora of model structures on double categories whose homotopy theories encode different 2-dimensional structures.
Based on work in preparation joint with Lyne Moser and Paula Verdugo.
Topos Institute Colloquium, 18th of September 2025.
———
Double categories are a flexible 2-dimensional setting that allows us to encode two types of morphisms between objects, as well as a notion of higher cells. Surprisingly, unlike most categorical structures, there is no canonical notion of “equivalence of double categories”, as it seems that every possible definition requires us to make a choice. In this talk we will illustrate the issue that arises when defining double-categorical equivalences. Then, we will show how we can use homotopy theory to give a decisive answer as to who the “canonical double categorical equivalences” should be: the gregarious equivalences introduced by Campbell. In the process, we will show how to construct a plethora of model structures on double categories whose homotopy theories encode different 2-dimensional structures.
Based on work in preparation joint with Lyne Moser and Paula Verdugo.
![[Oxford Seminar] David Corfield | Categorical systems theory: control and emergence](https://i.ytimg.com/vi/wSWmHZNjpzg/mqdefault.jpg "[Oxford Seminar] David Corfield | Categorical systems theory: control and emergence
Oxford Seminar, March 5 2026
Speaker: David Corfield
Also appearing in this recording are David Jaz Myers and Matteo Capucci.
Full Title: Categorical systems theory: control and emergence
Abstract: This will be an informal session with plenty of discussion time, investigating a couple of concepts that arise from the category-theoretic treatment of systems.
*(1) Control*
How inputs to a system regulate its behaviour. Starting points: (a) In response to the active inference program, some recent articles (e.g., https://arxiv.org/abs/2406.07577 and https://arxiv.org/abs/2508.06326) have looked to understand autonomous systems as composed of agent and controller subsystems, equipped with dual interfaces; (b) Ordinary Lyapunov functions have been treated category-theoretically (https://arxiv.org/abs/2502.15276), work that should be extendable to variants. Where ISS (input-to-state stability) Lyapunov functions concern stability under any external perturbation, control Lyapunov functions concern stability under a chosen input.
*(2) Emergence*
Phenomena where the composite behaviour of the parts does not equate to the behaviour of the composite. Starting points: (a) Elie Adams thesis, Systems, Generativity and Interactional Effects (https://elieadam.com/eadam_PhDThesis.pdf); (b) Puca et al. on Failures of compositionality (https://arxiv.org/abs/2307.14461) (c) Erik Hoel on causal emergence (e.g., https://arxiv.org/abs/2202.01854). Two relevant CT constructions appear to be laxness of functors and coarse-graining as epimorphisms, potentially fitting well with a double category-theoretic outlook.")
![[TopOx] Tom Leinster: The many faces of magnitude](https://i.ytimg.com/vi/wxqfxRCGoOE/mqdefault.jpg "[TopOx] Tom Leinster: The many faces of magnitude
16th of February 2026. Slides available at https://topos.institute/events/topox/
The magnitude of a square matrix is the sum of all the entries of its inverse. This strange definition, suitably used, enables us to define the magnitude of many objects in different contexts across mathematics. All of them can be seen as measures of size. For example, the magnitude of a metric space combines classical quantities such volume, surface area, and dimension. The magnitude of a category is closely related to Euler characteristic. The magnitude of a graph is an invariant sharing features with the Tutte polynomial (but not a specialization of it). Magnitude also appears in the difficult problem of quantifying biological diversity: under certain circumstances, the greatest possible diversity of an ecosystem is exactly its magnitude. And there is now a theory of magnitude homology, which has the same relationship to magnitude as ordinary homology does to Euler characteristic. I will give an aerial view of this landscape.")
![[Oxford Seminar] Matthew Daggit | Developing support for end-to-end verification of neural AI agents](https://i.ytimg.com/vi/xK8Kw-g0mNs/mqdefault.jpg "[Oxford Seminar] Matthew Daggit | Developing support for end-to-end verification of neural AI agents
Oxford Seminar, 1st of May 2025,
Full Title: Developing programming language support for end-to-end verification of neural AI agents
Over the past decade, there has been impressive progress in developing algorithms capable of formally verifying first-order, linear specifications about small-to-medium-sized neural networks. This has opened the door to formally verifying the correctness of neural AI agents operating in complex environments. However, due to the complexity of integrating these verification algorithms with other reasoning tools and the many moving parts involved, deploying them in practice has proven more challenging than anticipated.
In this talk, I will introduce Vehicle, a tool that my collaborators and I have been developing. Vehicle allows users to: (i) write specifications for AI agents in a high-level, domain-specific language; (ii) use these specifications to guide training; (iii) formally verify whether the resulting neural network satisfies the specification; and (iv) export verified specifications to interactive theorem provers where the agents can be reasoned in the context of their environment. In the talk I will highlight how we leverage type theory in unusual ways to improve the user experience, our use of real-valued logic semantics to interpret Boolean specifications, and finally some of the open theoretical challenges in the field.
Links:
https://github.com/vehicle-lang/vehicle")
![[DOTS Lectures] 6. Categories of Moore Machines](https://i.ytimg.com/vi/xMYGOzYhVVo/mqdefault.jpg "[DOTS Lectures] 6. Categories of Moore Machines
Part of a lecture series on the Double Operadic Theory of Systems (DOTS) presented by David Jaz Myers.")
![[2-torial] Owen tells Tim about elaborators for type theories [2/2]](https://i.ytimg.com/vi/xQSG_a_uyKk/mqdefault.jpg "[2-torial] Owen tells Tim about elaborators for type theories [2/2]
Accompanying code can be found on github: https://github.com/ToposInstitute/elaboratorial")
![[Berkeley Seminar] Aaron Huntley (Topos Institute) | Generalised coproduct completions](https://i.ytimg.com/vi/xa04dVG4fEs/mqdefault.jpg "[Berkeley Seminar] Aaron Huntley (Topos Institute) | Generalised coproduct completions
Title: Partial functions and other generalised coproduct completions
Abstract: The category of sets and functions is the free coproduct completion of the terminal category. In a double-categorical setting, Evan Patterson defined a new notion of double (co)product and used it to prove that the double category of sets, functions and spans is the free coproduct completion of the terminal double category. In this talk we both generalise and refine this notion. First, we extend Patterson’s original definition to include (co)products in (co)virtual double categories, which can capture examples such as coproducts in Span(C) even when C does not have pullbacks. Second, we isolate finer classes of double (co)products, denoted (L,R)-(co)products, where L and R are certain classes of functions. As an application, we exhibit the double category of sets, functions and partial functions as a free (L,R)-coproduct completion of the terminal double category.
Date: 9/1/2026")
![[Oxford Seminar] Adrián Puerto Aubel | A glance at Petri net theory](https://i.ytimg.com/vi/z5DXdfV8Fw0/mqdefault.jpg "[Oxford Seminar] Adrián Puerto Aubel | A glance at Petri net theory
Oxford Seminar, February 19 2026
Speaker: Adrián Puerto Aubel
Full Title: A glance at Petri net theory
Abstract: Petri nets are formal models of computing well-known for depicting true concurrency. Unlike automata, they overcome the state-space explosion problem by avoiding interleaving semantics. In this talk I will give an overview of the most prominent theoretical developments of more than 50 years of Petri net theory. This will range from the different expressions of formal semantics of these models as marking graphs, unfoldings, or event structures, to an overview of relevant problems defined on them and their complexities, with a particular focus on structural analysis techniques.")
