Uploaded June 2026 | Updated September 2026, 2 weeks ago
Topos Institute Colloquium, 25th of June 2026.
———
Over the course of a visit to the Hausdorff Institute in May 2024, Kevin Carlson, Reed Mullanix, and I had the pleasure of being the first group in the world to use the newly public Narya proof assistant for substantive formalisation. Despite our recurring initial sense of "our human brains are too puny for this labyrinthine complexity", we were successful in working out a toolbox of idioms that has since made reasoning about constructions in Displayed Type Theory [dTT] more tractable. By the end of the week, we arrived at a 73 non-whitespace loc definition of Kan complexes.
With six more lines, we can construct the singular semi-simplicial types and make the following theorem statement:
Sing.Kan (X : Type) : Kan (Sing X) := ?
This is an internal statement that "types are ∞-groupoids"; to give a term of this type would mean to get an internal uniform handle on all Kan filling operations associated to path-spaces.
We would like to prove this, and it is at this point that everything starts to go wrong!
The key distinction lies in the difference between a displayed and relative Kan structure. The former gives fillers of horns upstairs over prescribed fillers downstairs, while the latter gives fillers of horns upstairs over arbitrary fillers downstairs. This is related to the phenomenon in simplicial homotopy theory in which one is often forced to generalise theorems from the absolute case to the relative case. In dTT, however, the slice construction raises the degree of relativity, and one is then forced to generalise to working across all degrees of relativity at once.
In this talk, I will describe my work in progress with Reed Mullanix on constructing the missing shape/cofibration theory for dTT that would make such proofs possible. This will shift the notion of the syntax for a type theory to meaningfully constitute a higher dimensional object.
Topos Institute Colloquium, 25th of June 2026.
———
Over the course of a visit to the Hausdorff Institute in May 2024, Kevin Carlson, Reed Mullanix, and I had the pleasure of being the first group in the world to use the newly public Narya proof assistant for substantive formalisation. Despite our recurring initial sense of "our human brains are too puny for this labyrinthine complexity", we were successful in working out a toolbox of idioms that has since made reasoning about constructions in Displayed Type Theory [dTT] more tractable. By the end of the week, we arrived at a 73 non-whitespace loc definition of Kan complexes.
With six more lines, we can construct the singular semi-simplicial types and make the following theorem statement:
Sing.Kan (X : Type) : Kan (Sing X) := ?
This is an internal statement that "types are ∞-groupoids"; to give a term of this type would mean to get an internal uniform handle on all Kan filling operations associated to path-spaces.
We would like to prove this, and it is at this point that everything starts to go wrong!
The key distinction lies in the difference between a displayed and relative Kan structure. The former gives fillers of horns upstairs over prescribed fillers downstairs, while the latter gives fillers of horns upstairs over arbitrary fillers downstairs. This is related to the phenomenon in simplicial homotopy theory in which one is often forced to generalise theorems from the absolute case to the relative case. In dTT, however, the slice construction raises the degree of relativity, and one is then forced to generalise to working across all degrees of relativity at once.
In this talk, I will describe my work in progress with Reed Mullanix on constructing the missing shape/cofibration theory for dTT that would make such proofs possible. This will shift the notion of the syntax for a type theory to meaningfully constitute a higher dimensional object.
![[DOTS Lectures] 8. Compositionality of behaviours: generalized Moore machine case](https://i.ytimg.com/vi/Xxo8Om-pBn8/mqdefault.jpg "[DOTS Lectures] 8. Compositionality of behaviours: generalized Moore machine case
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")
![[Oxford Seminar] Tim Hosgood | Homotopy coherent Bousfield–Kan](https://i.ytimg.com/vi/Y9w6YzhEaoo/mqdefault.jpg "[Oxford Seminar] Tim Hosgood | Homotopy coherent Bousfield–Kan
Oxford Seminar, July 30 2026
You can view the listing for this talk online at https://topos.institute/events/oxford-seminar/talks/2026-07-30_hosgood_bousfield.html
Speaker: Tim Hosgood
Full Title: Homotopy coherent Bousfield–Kan
Abstract: From a weird little-known construction in complex geometry we can notice a new type of subdivision of simplices: half cubical, half simplicial, and very useful for working with certain geometric objects. These subdivisions are called /homotopy-coherent simplices/ (previously /wiggly simplices/).
In this talk I will give an introduction to the theory and methodology of homotopy limits of cosimplicial spaces through some tools of 2-category theory, explaining the important construction of Bousfield–Kan, and how this generalises to the homotopy coherent setting following joint work with Jason Brown and Cheyne Glass. I will also show lots of pictures of triangles. If times permits, I will introduce the notion of /homotopy homotopy limit/.
/Prerequisites./ The talk will use Quillen model categories and cosimplicial simplicial sets, but I will try to give good enough speedy overviews of both of these definitions. I will also use some definitions from enriched category theory (namely weighted (co)limits) but in a way that will likely make any Australians in the room rather upset.
/Recommended pre-reading./ The following definitions: nerve of a category, barycentric subdivision of a simplex, simplicial set.")
![[Berkeley Seminar] Mike Dodds (Galois) | What works and doesnt selling formal methods in industry](https://i.ytimg.com/vi/Z2bTpsO4fcc/mqdefault.jpg "[Berkeley Seminar] Mike Dodds (Galois) | What works and doesnt selling formal methods in industry
Title: What works and doesnt selling formal methods in industry
Abstract:I joined Galois to do research, but to my surprise I also learned how to sell formal methods to industry and government. In this talk I will explain what I think works, what doesn’t, and what it says about formal methods as a technology. The spoiler is that clients are rational, formal methods are expensive, and this makes most potential projects unviable. As SPECIAL BONUS CONTENT I will also talk about AI and why it will probably change everything.
Date: November 10, 2025")
![[Oxford Seminar] Greg Neustroev | The Treachery of Certificates: Ceci n’est pas une supermartingale](https://i.ytimg.com/vi/ZO7KmOXGX98/mqdefault.jpg "[Oxford Seminar] Greg Neustroev | The Treachery of Certificates: Ceci n’est pas une supermartingale
Oxford Seminar, June 25 2026
You can view the listing for this talk online at https://topos.institute/events/oxford-seminar/talks/2026-06-25_neustroev_treachery.html
Speaker: Greg Neustroev
Full Title: The Treachery of Certificates: Ceci n’est pas une supermartingale
Abstract: To prove that a stochastic system exhibits a desired behavior with high probability (for example, that it reaches a target while avoiding danger) it often suffices to produce a single function on its states satisfying a few pointwise inequalities: a supermartingale certificate. Finding such a function is the hard part; checking one is easy, which is why neural networks, as flexible function-searchers, have become a natural tool for the job.
But a certificate is a static object — a function you can write down — while the object that actually carries the proof is a stochastic process: its dynamic interpretation as it rides the systems randomness. These are not the same thing, and the passage between them is not canonical: one function can induce many supermartingales, depending on how we stop, shift, or time-compensate it. Well build both objects from scratch, make the construction explicit, and see why conflating them — a common slip, even among practitioners — is exactly where soundness is won or lost.")
![[Berkeley Seminar] Benjamin Brast-McKie | Programmatic Semantics](https://i.ytimg.com/vi/ZqTpdJKHT_4/mqdefault.jpg "[Berkeley Seminar] Benjamin Brast-McKie | Programmatic Semantics
Title: Programmatic Semantics
Abstract: This talk presents a programmatic methodology which uses the model-checker software that I developed to rapidly prototype semantic theories.
I will begin by presenting a standard methodology in philosophical logic to highlight a number of shortcomings which motivate the programmatic methodology. I will then introduce the model-checker which draws on the SMT solver Z3 to rule out finite countermodels of a user specified size, providing evidence that a logical consequences has no countermodels if in fact there are none. Implementing a programmatic semantics with the model-checker extends the standard methodology by easing the process of exploring and prototyping novel semantic theories.
In addition to facilitating the study of complex semantic theories, the model-checker provides resources for uploading semantic theories to the TheoryLib to facilitate collaboration. Programmatic semantic theories are also modular, making them easy to combine and compare, allowing users to survey the interactions in languages with many operators. Moreover, the computability of a semantic theory provides an objective measure that may be weighed alongside other theoretical virtues.
Although the model-checker is a general purpose utility for working in semantics, applications in hyperintensional semantics are particularly natural given the increased complexity of these semantic systems. Rather than a deficiency, I will characterize well-motivated forms of theoretical complexity as a sign of the maturity of semantics as a discipline. It is in support of both the future development and accessibility of semantics that the model-checker aims to make a contribution. The talk will conclude with a brief demonstration to make the workflow concrete.
Date: 2025-06-17
https://topos.institute/events/berkeley-seminar/")
