Uploaded June 2026 | Updated September 2026, 2 weeks ago
Topos Institute Colloquium, 11th of June 2026.
———
Both continuous and discrete time dynamical systems have natural notions of stability, and they both admit a Lyapunov theory which classifies stable equilibria. In prior work, we gave a categorical treatment of Lyapunov theory using coalgebras which recovers the continuous and discrete time theories and more as special cases. Many systems that occur in applications are neither purely discrete nor purely continuous in their behavior. Such "hybrid dynamical systems" may exhibit a continuous evolution of state for some time and then make a sudden discontinuous jump. The classic example is a bouncing ball, where an impact with the ground instantaneously changes both the direction and magnitude of the ball's velocity. New types of behavior emerge in hybrid systems. Zeno stability is when the system undergoes infinitely many discrete jumps in finite time (again, think of the bouncing ball). We encode hybrid systems as coalgebras in order to apply our categorical Lyapunov theory. Doing so requires the use of a category of charts, blending the categories of manifolds and sets, as well as a novel endofunctor blending tangent bundle and powerset. This recovers Zeno stability as a special case as well as Lyapunov-type results for certifying Zeno stability that have appeared in the literature. We demonstrate this theory on Lagrangian hybrid systems (mechanical systems with collision) and hybrid periodic orbits (bipedal walking).
Topos Institute Colloquium, 11th of June 2026.
———
Both continuous and discrete time dynamical systems have natural notions of stability, and they both admit a Lyapunov theory which classifies stable equilibria. In prior work, we gave a categorical treatment of Lyapunov theory using coalgebras which recovers the continuous and discrete time theories and more as special cases. Many systems that occur in applications are neither purely discrete nor purely continuous in their behavior. Such "hybrid dynamical systems" may exhibit a continuous evolution of state for some time and then make a sudden discontinuous jump. The classic example is a bouncing ball, where an impact with the ground instantaneously changes both the direction and magnitude of the ball's velocity. New types of behavior emerge in hybrid systems. Zeno stability is when the system undergoes infinitely many discrete jumps in finite time (again, think of the bouncing ball). We encode hybrid systems as coalgebras in order to apply our categorical Lyapunov theory. Doing so requires the use of a category of charts, blending the categories of manifolds and sets, as well as a novel endofunctor blending tangent bundle and powerset. This recovers Zeno stability as a special case as well as Lyapunov-type results for certifying Zeno stability that have appeared in the literature. We demonstrate this theory on Lagrangian hybrid systems (mechanical systems with collision) and hybrid periodic orbits (bipedal walking).
![[DOTS Lectures] 4. Composing Moore Machines](https://i.ytimg.com/vi/jsM2jTuT_Zc/mqdefault.jpg "[DOTS Lectures] 4. Composing Moore Machines
Part of a lecture series on the Double Operadic Theory of Systems (DOTS) presented by David Jaz Myers.")
![[2-torial] David Jaz tells Brendan about a topos-theoretic interpretation for conceptual modelling](https://i.ytimg.com/vi/kFQpKp-ehZI/mqdefault.jpg "[2-torial] David Jaz tells Brendan about a topos-theoretic interpretation for conceptual modelling
Recorded at the Oxford Office on the 5th of December 2025.")
![[DOTS Lectures] 1. Categories of systems](https://i.ytimg.com/vi/kZ4muU5Wc_4/mqdefault.jpg "[DOTS Lectures] 1. Categories of systems
Part of a lecture series on the Double Operadic Theory of Systems (DOTS) presented by David Jaz Myers.")
![[Berkeley Seminar] Raph Levien | How Rust won: the quest for performant, reliable software](https://i.ytimg.com/vi/k_-6KI3m31M/mqdefault.jpg "[Berkeley Seminar] Raph Levien | How Rust won: the quest for performant, reliable software
Title: How Rust won: the quest for performant, reliable software
Abstract: For a long time, high performance has been in tension with reliability. In particular, languages designed for high performance were not memory safe, with real implications for unexpected crashes and security vulnerabilities. Rust is the first practical language to address this tension, building on affine types and other principles programming language theory, synthesized with an attention to low level systems programming. Rust’s success emerged not just from a clever idea, but consistently excellent execution and the formation of a strong community around the language. This talk will discuss several aspects of what Rust got right, as well as the rocky journey of ideas from academic theory to real world impact.
Slides: https://docs.google.com/presentation/d/1SoDsm_m_pb_gS6Y98HghhzBviYZxp3F2XawhIppJQQo/edit?usp=sharing
https://topos.institute/events/berkeley-seminar/")
![[DOTS Lectures] 11. A general representability theorem for Systems Theory Pt. 1](https://i.ytimg.com/vi/kpmhI1oHGnM/mqdefault.jpg "[DOTS Lectures] 11. A general representability theorem for Systems Theory Pt. 1
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")
![[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.")
