Uploaded April 2026 | Updated September 2026, 2 weeks ago
Topos Institute Colloquium, 9th of April 2026.
———
In information-theoretic terms, a map is continuous when a finite
amount of information about its input suffices for computing a finite
amount of information about its output. Already Brouwer observed that
this allows one to represent a continuous functional from sequences to
numbers with a certain well-founded question-answer tree.
In type theory, a second-order functional is a (dependently typed) map
F : (∏(a : A) . P a) → (∏(b : B) . Q b).
Its continuity is once again witnessed by B-many well-founded trees
whose nodes are “questions” a : A, the branches are indexed by
“answers” p : P a, and the leaves are “results” Q b. In this work, we
observe that such tree representations can be expressed in purely
category-theoretic terms, using the notion of right T-comodules for
the monad T of well-founded trees on the category of containers. A
tree representation for F is then just a Kleisli map for the monad T.
Doing so exposes a rich underlying structure, and immediately suggests
generalisations: any right T-comodule for any monad T on containers
gives rise to a corresponding representation theorem for second-order
functionals. We give several examples of these, ranging from finitely
supported functionals, to functionals that can query their input just
once (or sometimes not at all), to functionals that can additionally
interact with their environment, to partial functionals, to observing
that any functional can be trivially represented by itself.
This is joint work with Andrej Bauer from the University of Ljubljana.
Topos Institute Colloquium, 9th of April 2026.
———
In information-theoretic terms, a map is continuous when a finite
amount of information about its input suffices for computing a finite
amount of information about its output. Already Brouwer observed that
this allows one to represent a continuous functional from sequences to
numbers with a certain well-founded question-answer tree.
In type theory, a second-order functional is a (dependently typed) map
F : (∏(a : A) . P a) → (∏(b : B) . Q b).
Its continuity is once again witnessed by B-many well-founded trees
whose nodes are “questions” a : A, the branches are indexed by
“answers” p : P a, and the leaves are “results” Q b. In this work, we
observe that such tree representations can be expressed in purely
category-theoretic terms, using the notion of right T-comodules for
the monad T of well-founded trees on the category of containers. A
tree representation for F is then just a Kleisli map for the monad T.
Doing so exposes a rich underlying structure, and immediately suggests
generalisations: any right T-comodule for any monad T on containers
gives rise to a corresponding representation theorem for second-order
functionals. We give several examples of these, ranging from finitely
supported functionals, to functionals that can query their input just
once (or sometimes not at all), to functionals that can additionally
interact with their environment, to partial functionals, to observing
that any functional can be trivially represented by itself.
This is joint work with Andrej Bauer from the University of Ljubljana.
![[DOTS Lectures] 14. Applying the representability theorem: examples of compositional behaviours](https://i.ytimg.com/vi/RNwCljKiP24/mqdefault.jpg "[DOTS Lectures] 14. Applying the representability theorem: examples of compositional behaviours
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")
![[Berkeley Seminar] CB Aberle: All Concepts are Essentially Algebraic](https://i.ytimg.com/vi/RmiTOa4b0bA/mqdefault.jpg "[Berkeley Seminar] CB Aberle: All Concepts are Essentially Algebraic
Title: All Concepts are Essentially Algebraic
Abstract: Lawveres categorical formulation of algebraic theories enables one to study some of the most common structures found in mathematics – e.g. groups, rings, etc. – at a high level of precision and generality. However, many significant mathematical concepts, including categories, topological spaces, etc., turn out not to be algebraic, in this sense. Notably, the very framework used by Lawvere to describe algebraic theories and their models – categories with finite products and product-preserving functors between them – cannot be described as an algebraic theory, and so it seems that algebra alone cannot encompass the whole of mathematics (nor even itself). There is, however, a deeper sense in which all of mathematics is essentially algebraic. What is needed to reveal this fact is to adapt the classical notion of algebraic theories, which are fundamentally simply typed, to an appropriate notion of dependently typed algebraic theories. At this level of generality, one is capable of defining not only individual mathematical structures, but structures that themselves encompass whole universes of mathematics, including topoi, models of type theory, etc. In particular, the theory of dependently-typed algebraic theories is itself describable as a dependently-typed algebraic theory. This fact has many profound consequences, of which I shall highlight just one: using the framework of dependently-typed algebraic theories, one can construct a type theory whose types themselves correspond to type theories, with functions between these types corresponding to translations between the corresponding type theories.
https://topos.site/events/berkeley-seminar/")
![[Berkeley Seminar] David Espinosa: Monad translations compose](https://i.ytimg.com/vi/Snvwc4JVIYc/mqdefault.jpg "[Berkeley Seminar] David Espinosa: Monad translations compose
Title: Monad Translations Compose
Abstract: Many people have observed that monad translations compose. We give this idea a try using the ML module system and see what mileage we can get out of it.
https://topos.site/events/berkeley-seminar/")
![[2-torial] Categorical algebraic geometry, Part 1](https://i.ytimg.com/vi/SwnZ_i0t86g/mqdefault.jpg "[2-torial] Categorical algebraic geometry, Part 1
2-torial, July 28 2026
Speaker: Tim Hosgood
There are many approaches to algebraic geometry, and many different ways to arrive at the subject. Here were going to take an incredibly specific and biased approach: what if you already love 2-categories and want to be able to say the phrase fpqc sheaf as quickly as possible, but not /too/ quickly? In this series of exercises we will build towards an understanding of *relative algebraic geometry*, which allows us to work in arbitrary (nice) symmetric monoidal categories.
*Prerequisites.* Quotients of rings, Yoneda embedding, 2-limits, symmetric monoidal categories (cosmoi).
*Key concepts.* Functor of points, affine scheme, quasi-coherent sheaf, Grothendieck pseudofunctor, pre-topology, faithfully flat topology, algebra over a commutative monoid, sheaf, affine scheme (again).
*Further reading.*
- Bertrand Toën, Michel Vaquié, Under Spec Z. [arXiv:math/0509684]
- Bertrand Toen, Gabriele Vezzosi, Homotopical Algebraic Geometry II: geometric stacks and applications. [arXiv:math/0404373]
[arXiv:math/0509684] https://arxiv.org/abs/math/0509684
[arXiv:math/0404373] https://arxiv.org/abs/math/0404373")
![Rory Lucyshyn-Wright: V-graded categories [...] for enrichment and actions of monoidal categories](https://i.ytimg.com/vi/UR9LUUfaJiM/mqdefault.jpg "Rory Lucyshyn-Wright: V-graded categories [...] for enrichment and actions of monoidal categories
Topos Institute Colloquium, 24th of April 2025.
———
Enriched categories have hom-objects in a monoidal category V, but their theory is usually formulated under the assumption that V is biclosed and so is enriched in itself. Categories equipped with an action of V (or V-actegories) provide a related setting with the advantage that an arbitrary monoidal category V can always be regarded as a V-actegory. Richard Wood delineated a setting subsuming both V-enriched categories and V-actegories by considering V-graded categories, which are categories enriched in a monoidal category of presheaves on V but admit also a direct and elementary definition in terms of a notion of morphism with an additional parameter in V. Graded categories have also been called procategories (by Kelly-Labella-Schmitt-Street) and locally V-graded categories (by Levy).")
