![[TopOx] Steve Awodey: Path Types in Algebraic Type Theory @ToposInstitute](https://i.ytimg.com/vi/lanvZuki4qQ/maxresdefault.jpg)
Uploaded May 2026 | Updated September 2026, 2 weeks ago
18th of May 2026. Slides available at https://topos.institute/events/topox/
A representable natural transformation u : U* → U in the category Psh(C) of presheaves on a small category C is a “natural model" of dependent type theory. The type-forming operations may be described as an algebraic structure on u, representing corresponding operations on the type-families classified by u. For example, the dependent product or “Pi-type” is an algebra structure for the polynomial endofunctor
P_u : Psh(C) → Psh(C) .
Similar operations on u represent the other type-formers of unit type, dependent sums, and identity types. The latter are given by a recently determined “path-type” structure, which relates such models to cubical (Quillen) model categories.
18th of May 2026. Slides available at https://topos.institute/events/topox/
A representable natural transformation u : U* → U in the category Psh(C) of presheaves on a small category C is a “natural model" of dependent type theory. The type-forming operations may be described as an algebraic structure on u, representing corresponding operations on the type-families classified by u. For example, the dependent product or “Pi-type” is an algebra structure for the polynomial endofunctor
P_u : Psh(C) → Psh(C) .
Similar operations on u represent the other type-formers of unit type, dependent sums, and identity types. The latter are given by a recently determined “path-type” structure, which relates such models to cubical (Quillen) model categories.
![[TopOx] Steve Awodey: Path Types in Algebraic Type Theory](https://i.ytimg.com/vi/lanvZuki4qQ/mqdefault.jpg "[TopOx] Steve Awodey: Path Types in Algebraic Type Theory
18th of May 2026. Slides available at https://topos.institute/events/topox/
A representable natural transformation u : U* → U in the category Psh(C) of presheaves on a small category C is a “natural model of dependent type theory. The type-forming operations may be described as an algebraic structure on u, representing corresponding operations on the type-families classified by u. For example, the dependent product or “Pi-type” is an algebra structure for the polynomial endofunctor
P_u : Psh(C) → Psh(C) .
Similar operations on u represent the other type-formers of unit type, dependent sums, and identity types. The latter are given by a recently determined “path-type” structure, which relates such models to cubical (Quillen) model categories.")
![[DOTS Lectures] 17. Representability for double operad algebras](https://i.ytimg.com/vi/larbRprPuPM/mqdefault.jpg "[DOTS Lectures] 17. Representability for double operad algebras
Part of a lecture series on the Double Operadic Theory of Systems (DOTS) presented by David Jaz Myers.
Some material from these lectures can be found in Davids book on categorical systems theory:
https://www.davidjaz.com/Papers/DynamicalBook.pdf")
![[DOTS Lectures] 3. Moore machines](https://i.ytimg.com/vi/m-HDSZ0iNWE/mqdefault.jpg "[DOTS Lectures] 3. Moore machines
Part of a lecture series on the Double Operadic Theory of Systems (DOTS) presented by David Jaz Myers.")
![[2-torial] Toposes: from topological spaces to databases](https://i.ytimg.com/vi/mNFibqlr_Bk/mqdefault.jpg "[2-torial] Toposes: from topological spaces to databases
[2-torial] Toposes: from topological spaces to databases")
![[Berkeley Seminar] Evan Patterson | A uniform type theory for internal languages of cat. structures](https://i.ytimg.com/vi/mknZxNcn0Ho/mqdefault.jpg "[Berkeley Seminar] Evan Patterson | A uniform type theory for internal languages of cat. structures
Title: A uniform type theory for internal languages of categorical structures
Abstract: A hallmark of categorical logic is the interplay between category theory and type theory. A categorical structure can provide the semantics of a type theory; in the other direction, type theory can be used to describe the internal language of a categorical structure. The internal language is an ergonomic notation, based on elements and function application, to specify morphisms in the category. Typically, discovering an internal language is a bespoke process, performed anew for each categorical structure of interest. In this talk, we propose a uniform type theory giving internal languages for much of the “substructural” hierarchy of categorical logic, including such structures as categories, multicategories (planar, symmetric, and cartesian), PROPs, Lawvere theories, (symmetric) monoidal categories, cartesian categories, and Markov categories. The framework builds on the speaker’s work in double-categorical logic, and is described in preliminary form at: https://next.catcolab.org/rfc/0004
Date: May 26, 2026")
![[Oxford Seminar] Matteo Capucci | 2-classifiers for 2-algebras](https://i.ytimg.com/vi/mpHnD7peDS8/mqdefault.jpg "[Oxford Seminar] Matteo Capucci | 2-classifiers for 2-algebras
Oxford Seminar, 26th of June 2025
In this talk I will report on work in progress, joint with David Jaz Myers, about lifting discrete opfibration classifiers (2-classifiers, i.e. a Set-like object) from a 2-category K to the 2-category of algebras of a 2-monad T. In the setting of DOTS, we often construct behaviour functors as representables, but without a 2-classifier one cant really call these representables. Moreover, there is a strong connection between compositionality of such functors, the properties of the algebra they map out of, and the properties of the object(s) that represents them. These phenomena are in fact completely general, so we set out to better understand the situation and found some frankly interesting notions and results, chiefly a tight result on the existence of 2-classifiers for 2-algebras.")
![[Oxford Seminar] Nathan Haydon | Peirce’s Existential Graphs](https://i.ytimg.com/vi/oMDDqZsVlJE/mqdefault.jpg "[Oxford Seminar] Nathan Haydon | Peirce’s Existential Graphs
Oxford Seminar, 3rd of July 2025
Title: The second (graphical) calculus of relations: Peirce’s Existential Graphs
Abstract: C.S. Peirce’s Existential Graphs are a precursor to string diagrams as we know them today. In this talk I’ll discuss the assumptions that led Peirce to develop the graphs and give an overview of how Peirce’s work inspired recent developments in categorical logic.")
![[Berkeley Seminar] Hugo Paquet | Lazy categorical semantics of discrete probabilistic programming](https://i.ytimg.com/vi/oVsGsyDRFyQ/mqdefault.jpg "[Berkeley Seminar] Hugo Paquet | Lazy categorical semantics of discrete probabilistic programming
Title: Lazy categorical semantics of discrete probabilistic programming
Abstract: A lazy program interpreter postpones computation until the result is actually needed. This is typically more efficient than an eager (or call-by-value) interpreter, but the semantics is not generally the same.
In this talk I will discuss a new categorical semantics of lazy evaluation for algebraic effects, that relies on a subtle combination of name generation and read-only state. This semantic model suggests better intermediate representations of sum and product types in a lazy interpreter.
The practical motivation for this work is a real-world application of probabilistic programming, in which large algebraic data types cause significant performance issues. As I will explain, since probabilistic programming is described by an affine monad, one can use lazy evaluation to speed up the computation without affecting the semantics.
This is joint work with Simon Castellan (Inria, France).
Date: May 5, 2026")
