Uploaded June 2026 | Updated September 2026, 2 weeks ago
Topos Institute Colloquium, 18th of June 2026.
———
Authors: Richard Blute, Robin Cockett, Durgesh Kumar, J.S. Lemay
A result of Coecke, Pavlovic and Vicary states that a basis for a finite-dimensional Hilbert space can be equivalently characterised as a commutative dagger-Frobenius monoid in the category of finite-dimensional Hilbert spaces. This can be extended to an equivalence between such Frobenius algebras and the category of finite sets.
We describe an ongoing project to attempt to extend this result beyond finite sets. This
requires on the one hand replacing the category of sets with the category of Ehrhard’s
finiteness spaces, one of the motivating examples for the theory of differential linear logic. On
the other hand, Frobenius algebras must be replaced by linear monoids as defined by Priyaa
Srivinvasan.
Topos Institute Colloquium, 18th of June 2026.
———
Authors: Richard Blute, Robin Cockett, Durgesh Kumar, J.S. Lemay
A result of Coecke, Pavlovic and Vicary states that a basis for a finite-dimensional Hilbert space can be equivalently characterised as a commutative dagger-Frobenius monoid in the category of finite-dimensional Hilbert spaces. This can be extended to an equivalence between such Frobenius algebras and the category of finite sets.
We describe an ongoing project to attempt to extend this result beyond finite sets. This
requires on the one hand replacing the category of sets with the category of Ehrhard’s
finiteness spaces, one of the motivating examples for the theory of differential linear logic. On
the other hand, Frobenius algebras must be replaced by linear monoids as defined by Priyaa
Srivinvasan.
![[Oxford Seminar] David Jaz Myers | Composing flavoured Petri nets](https://i.ytimg.com/vi/s793leHjc_4/mqdefault.jpg "[Oxford Seminar] David Jaz Myers | Composing flavoured Petri nets
Oxford seminar, 28th of August 2025
Abstract: Well describe a doctrine of various flavors of Petri nets in the double operadic theory of systems framework.")
![[Oxford Seminar] David Jaz Myers | Compositionality of Flavoured Petri Nets](https://i.ytimg.com/vi/sQW9KI9hdTI/mqdefault.jpg "[Oxford Seminar] David Jaz Myers | Compositionality of Flavoured Petri Nets
Oxford Seminar, 11th of September 2025
In this talk, we will see a natural notion of nesting composition for flavoured Petri nets: Petri nets whose places and transitions come with extra data determined by a symmetric monoidal double category and which determine the intended semantics of the Petri net.")
![[Berkeley Seminar] Owen Lynch | Abstract interpretation for semi-dependent type theories](https://i.ytimg.com/vi/tAKqODzU908/mqdefault.jpg "[Berkeley Seminar] Owen Lynch | Abstract interpretation for semi-dependent type theories
Title: Abstract interpretation for semi-dependent type theories
Abstract: ML-style module systems have a long and rich history which ultimately stems back to Lawvere’s seminal work on algebraic theories. While ML-style module systems have typically been confined to ML-descendants, analogous PL constructs that may be more familiar include Java-style interfaces or Haskell-style type classes. In my research for SGAI, I have adopted the perspective that module signatures are the appropriate programming language analogue for theories in a variety of doctrines of categorical algebra. Classical module signatures as found in ML can be are syntactic presentations of “theories for the doctrine of cartesian closed categories”; it is productive to vary “cartesian closed category” to “cartesian category”, “finite limit category”, “regular hyperdoctrine” (the categorical version of a restricted form of first-order logic), “symmetric monoidal categories”, etc. Then the module language for a doctrine extends the well-known internal language for the doctrine by adding “genericism”. For instance, it is well-known that the internal language of a symmetric monoidal category is given by a “linear do notation” where each variable may only be consumed once. However, typically an implementation of this internal language would fix a specific symmetric monoidal category. The module language allows varying the symmetric monoidal category, and potentially migrating expressions between various symmetric monoidal categories. This is of interest to SGAI because presentations of symmetric monoidal categories (e.g., module signatures for the symmetric monoidal doctrine) are Petri nets, and morphisms between them (e.g., module functors for the symmetric monoidal doctrine) are “hierarchical Petri nets”, where each transition in the codomain Petri net is associated with a process in the domain Petri net. Other applications to the SGAI program include the observation, going back to early work in ACT by Spivak, that databases schemas are productively thought of as theories in certain doctrines, with the choice of doctrine depending on the feature-set of the database engine.
Date: 2025-12-09")
![[Oxford Seminar] Jason Brown | Wreaths in Span(Set)](https://i.ytimg.com/vi/tbnRgqf81_A/mqdefault.jpg "[Oxford Seminar] Jason Brown | Wreaths in Span(Set)
Oxford Seminar, 2nd of October 2025
Abstract:
Steve Lack and Ross Street introduced wreaths as a generalisation of distributive laws between monads in their paper The formal theory of Monads II. This paper presents a nice story about how wreaths arise from considering the free completion of a 2-category under Kleisli objects and provides some interesting examples of wreaths. In particular, it is shown that orthogonal factorisation systems on a category can be expressed as wreaths in Span(Set).
In this talk well try to understand general wreaths in Span(Set) as expressing a weaker notion of factorisation system on a category. Well relate these factorisation structures to both familial functors and crossed double categories, and also present examples of where they naturally occur.")
![[Berkeley Seminar] Michael Arntzenius | UC Berkeley](https://i.ytimg.com/vi/tj9n1m9dNuY/mqdefault.jpg "[Berkeley Seminar] Michael Arntzenius | UC Berkeley
Title: A type system for finitely supported functions via pointed sets, Part 1
ABSTRACT:
Finite maps, in the form of dictionaries, associative arrays, or tables, are a key data type in most language’s standard libraries, but constructing and manipulating them is generally very explicit and loopful. In this talk I’ll demonstrate work in progress on a type system that can guarantee that functions written directly as lambda-expressions are finitely supported, and therefore can be represented as tables. This yields a higher-level, more declarative syntax, similar to logic programming languages or database query languages.
The semantics of my language live in Set, the category of pointed sets and point-preserving maps. In order to define the support of a function f: A → B, one needs a point nil ∈ B; then support f = {x ∈ A : f x ≠ nil}. In fact, finitely supported maps form a graded monad on Set; they are graded by their domain A. To fully flesh out the semantics and type system, I also need the free/forgetful adjunction between Set and Set*.
Unfortunately the typing rules get quite complex. I’d like to know if there’s a simpler way to accomplish the same goals, or a simpler or more general framework for presenting the type system itself.
Paper preprint for the interested: https://www.rntz.net/files/finite-functional-programming.pdf
Date: March 31, 2026")
![[2-torial] Owen tells Tim about elaborators for type theories [1/2]](https://i.ytimg.com/vi/uBjuFDs-shw/mqdefault.jpg "[2-torial] Owen tells Tim about elaborators for type theories [1/2]
Accompanying code can be found on github: https://github.com/ToposInstitute/elaboratorial")
![[2-torial] Quantum information theory, Part 1: Some linear algebra](https://i.ytimg.com/vi/uQ7hL9aaPYA/mqdefault.jpg "[2-torial] Quantum information theory, Part 1: Some linear algebra
2-torial, May 20 2026
You can find accompanying notes and other information on this video at https://topos.institute/work/lectures/2-torials/2026-05-20_hosgood_quantum/
Tutor: Tim Hosgood
Tutee: Jason Brown
The elements of quantum information theory are not so complicated: some linear algebra over the complex numbers and a bit of classical probability theory. But it doesnt take long before you run into some intriguing problems that showcase how established experimental results contradict our classical intuition. In this 2-torial we will learn the very basics of quantum theory, see how a Mach–Zehnder interferometer gives a real-world implementation of a classically impossible construction and suggests that we should go all in on complex numbers, and finally how this all applies to the world of theoretical bird watching via the Quantum Zeno effect.")
