SPRING 2025 Program
Fridays 1-3pm in BH 255A
(Anti-chronological order)
January 24, Mathieu Anel — Constructing higher elementary topoi
I will explain a strategy to construct examples of higher categories with a topos flavour (and morally supporting an interpretation of HoTT). The basic notion will be that of an LCC ∞-pretopos, since such a category always has enough univalent families. Every 1-pretopos has an ∞-pretopos envelope and I will show that the latter is LCC if the former is LCC and has enough projective objects. This can be apply to build higher envelope for realizability 1-topoi. (This is joint work with Steve and Reid.)
February 7, Romain Büchi — Legendre on the Distribution of Primes: A Case Study in the Art of Forming Mathematical Conjectures.
To make conjectures is an essential part of mathematical practice. A good conjecture can captivate generations of mathematicians and shape the development of entire fields. In this talk, I would like to examine one particular case: Legendre's conjecture of what is now known as the prime number theorem. Considering that it took a century to prove, this is a rather extraordinary case of conjecturing. However, by reconstructing the epistemological context, in which Legendre formulated and refined his conjecture, I will try to show that it was not the result of a lucky guess, or mere hunch. Legendre may have had an exceptional intuition that led him to "see the end from afar" (to borrow Poincaré's words). But he also had reasons to believe in the truth of the proposition he had found. And as we shall see, these reasons were of different kinds: numerical, one might say empirical, on the one hand, and on the other, more conceptual and linked to a sieve method he had developed.
February 14, Corinthia Aberlé — Fundamental Theorems for Free – Categorical Perspectives on Canonicity, Parametricity & Beyond
Logical relations are a powerful proof technique that can be used to prove properties of type systems such as normalization, canonicity, and parametricity, that typically evade straightforward proof by induction. But what is a logical relation? The usual way of introducing logical relations is by example, with the term "logical relations" being applied to anything that sufficiently resembles other logical relations arguments, rather than having a precise definition. This lack of precision makes for difficulty in extending logical relations arguments to novel type systems, since there is not a clear standard by which to judge whether the relations one defines are the "right" ones. In this talk, I will outline some of my own recent work on developing logical relations to prove parametricity theorems for substructural type systems, such as linear and ordered type theory, using this as a jumping-off point to discuss a more general categorical recipe for logical relations, that can be used to derive these and other examples.
February 21, Reid Barton — Ultraproduct models of homotopy type theory
Ultrapowers and ultraproducts are constructions used in model theory that produce models of "nonstandard" flavor, e.g., the hyperreals (a nonarchimedean real closed field). I will review these constructions and then explain how they can be applied to produce "nonstandard" models of homotopy type theory. These models are expected to correspond to ultraproducts of elementary ∞-topoi, such as ultrapowers of the ∞-category of spaces. While models of this kind have a standard internal logic, the corresponding elementary ∞-topoi contain exotic objects such as N-spheres for nonstandard natural numbers N. This talk will be mostly expository, mixed with a fair amount of speculation.
February 28, Christopher Dean (Dalhousie University) — Abstract Grothendieck fibrations and directed path objects
A tribe is a convenient framework for reasoning about the path-lifting properties of isofibrations in abstract homotopy theory. This talk will introduce a directed analogue of a tribe, which I call a ditribe, that additionally axiomatically captures the cartesian-lifting properties of Grothendieck fibrations and opfibrations. Ditribes have directed path objects; these are factorisations of diagonals with lifting properties that closely resemble those of path objects in a tribe. I will discuss a variety of higher categorical examples, including a complicial set model in which the directed path objects are lax arrow objects. The overarching goal of this work is to establish that, just as tribes serve as a convenient 1-categorical middle ground between the weak world of (∞,1)-categories and the strict syntax of homotopy type theory, ditribes provide a convenient middle ground between the world of (∞,n)-categories and a future syntax of directed homotopy type theory.
March 7, Spring Break — no seminar
March 14, Corinthia Aberlé and Steve Awodey — Tiny types
According to Lawvere, an object T in a category C is *tiny* if the exponentiation functor (-)^T : C —> C is a left adjoint. There are rather few such objects in the category Set, but they play a significant role in some other settings such as Synthetic Differential Geometry, HoTT, and elsewhere. In this two part talk we first introduce the notion of tinyness and show that it is also important in the semantics of dependent type theory. In the second part, we demonstrate some significant applications of this notion for internalizing parametricity and developing internal type-theoretic languages for arbitrary presheaf categories & Grothendieck topoi.
March 21, Owen Milner — Prospectus
This talk will be later than usual (2-4pm).
March 28, Claymont retreat — ( no seminar)
April 11, Harrison Grodin— A Domain-Theoretic Semantics for Recursive Types
Functional programming languages often include recursive types, allowing programmers to define types satisfying a given isomorphism. Such types cannot all be interpreted as sets, but they can be understood using domain theory. We consolidate and present foundational techniques in domain theory to understand programming languages with recursive types from a categorical perspective. We define a category of domains with finite coproducts, a symmetric monoidal closed structure for eager products and functions, and least solutions of recursive domain equations, whose objects are retracts of a universal space and whose morphisms are continuous with respect to a topology of approximations. paper
April 25, Greg Langmead— Discrete differential geometry in homotopy type theory (Master Defense)
Type families on higher inductive types such as pushouts can capture homotopical properties of differential geometric constructions including connections, curvature, and vector fields. We define a class of pushouts based on simplicial complexes, then define principal bundles, connections, and curvature on these. We provide an example of a tangent bundle but do not prove when these must exist. We define vector fields, and the index of a vector field. Our main result is a theorem relating total curvature and total index, a key step to proving the Gauss-Bonnet theorem and the Poincaré-Hopf theorem, but without an existing definition of Euler characteristic to compare them to. We draw inspiration in part from the young field of discrete differential geometry, and in part from the original classical proofs, which often make use of triangulations and other discrete arguments.
Thesis, slides, and video available here.
May 2, Double Feature : Two short talks on Compiling HoTT with Lean
Wojciech Nawrocki — Syntax and interpretation
Synthetic theories simplify mathematical developments by providing domain-specific languages in which certain constructions become more direct. Homotopy type theory (HoTT) is a synthetic framework for abstract homotopy theory. Although many proof assistants, such as Cubical Agda, support reasoning with synthetic theories, very few of the intended models of these synthetic constructions have been formalized in a proof assistant. This makes it impossible to formally establish results in classical mathematics using synthetic methods. To demonstrate that proof assistants can assist in interpreting synthetic proofs, we are formalizing the model theory of HoTT0, a simplified fragment of HoTT (with a restricted univalence axiom), in Lean. We present ongoing work that implements HoTT0 as an embedded domain-specific language in Lean. Our aim is to provide users with a library of macros that allow unfolding synthetic HoTT0 constructions into elements of the model, and soundly transferring HoTT0 proofs to classical proofs of statements about groupoids. Our code is available at sinhp.github.io/groupoid_model_in_lean4.
Spencer Woolfson — The groupoid model of HoTT0
HoTT0 restricts the univalence axiom to only hold on subuniverses of 0-truncated types (i.e. sets). Despite its limiting appearance, this suffices to develop significant portions of univalent, set-level mathematics expressible in HoTT. Building on prior work that modeled type theory in 1-groupoids using categories with families, we adapt this approach to natural model semantics based on polynomial functors. The natural model semantics are modular, allowing for implementations of other models of HoTT. This project also lays the groundwork for compiling other type theories in Lean. In this talk, I plan to discuss the formal system HoTT0, its 1-groupoid model, and show how some syntactic statements can be translated into classical proofs. I will also discuss what is gained by working in HoTT0, as opposed to extensional Martin-Löf type theory.
May 9, Nicola Gambino— On the commuting tensor product of symmetric multicategories and their bimodules
Given two algebraic theories S and T, their commuting tensor product is a new algebraic theory in which the operations of S and T are required to commute with each other. The analogue of this operation for symmetric operads is the famous Boardman-Vogt tensor product. A unified account of these commuting tensor products was given by Garner and Lopez-Franco. Here, we extend their analysis in two respects. First, we generalise it so as to make it applicable to the many-object case, recovering as special case the Boardman-Vogt tensor product of symmetric multicategories, subsuming work of Elmendorf and Mandell. Secondly, we investigate how the commuting tensor product acts on bimodules, generalising work of Dwyer and Hess.
Earlier seminars are listed here.