Carnegie Mellon University

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.)

January 24 —   no seminar

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,  Owen Milner —  Prospectus

February 28, Christopher Dean —  Surprise

March 7, Joseph Hua —  Groupoid quotients

March 14, Corinthia Aberlé —  Around tiny objects

March 21,  Reid Barton —  Ultraproducts of topoi

Just awesome!

March 28, Claymont retreat — ( no seminar)

Earlier seminars are listed  here.