StockholmGoteborgMeeting260422
Venue
11:30 - 12:15 Room EA, EDIT building, Chalmers campus, Göteborg
13:30 - 16:55 Room Analysen, EDIT building, Chalmers campus, Göteborg
Schedule
| 11:30 - 12:10 | Hugo Moeneclaey (chair: Peter Dybjer) |
| Lunch | |
| 13:30 - 14:10 | Peter LeFanu Lumsdaine (chair: Thierry Coquand) |
| 14:15 - 14:55 | Reid Barton |
| Coffee | |
| 15:30 - 16:10 | Fabian Grubmüller (chair: Robin Adams) |
| 16:15 - 16:55 | Chaitanya Leena Subramaniam |
| 18:00 | Dinner Andrum (map) |
Titles and abstracts
Hugo Moeneclaey: Severi-Brauer Varieties in Synthetic Algebraic Geometry
We reproduce a result from Châtelet’s thesis (1944) into synthetic algebraic geometry. A Severi-Brauer variety is an algebraic variety that is a projective space in some separable extension of the base ring. Châtelet’s result states that a Severi-Brauer variety with a point is a projective space. Our synthetic version of the theorem relies heavily on the internal version of étale sheafifcation. It is used both to define Severi-Brauer varieties and to reduce the problem to an easily answered question about matrix algebras. This respect the spirit of the original proofs, while giving a much more precise and concise formulation.
Peter LeFanu Lumsdaine: Makkai’s lost projectivity result
Several authors proved, around 1980, that intuitionistic higher-order/second-order systems admit a strong *rule of countable choice*: if they can prove “∀𝑛 : 𝑁 ∃𝑥 : 𝑋 𝜑 (𝑛, 𝑥)”, then in fact they can define a witnessing function 𝑁 → 𝑋. In particular, Makkai presented this for IHOL, formulated categorically — the natural numbers object in the free topos is projective; every cover 𝐴 ↠ 𝑁 splits. However, his proof (and others for higher-order systems) were never published at the time.
Henrik Forssell, Andrew Swan, and I recently completed an exposition of the proof, https://arxiv.org/abs/2604.01139, based on Makkai’s unpublished notes. The full treatment turns out to involve a fun tour through several topics in categorical logic: elementary toposes, indexed categories, arithmetic universes… I will aim to give an accessible presentation of the result, assuming as little background as possible.
Reid Barton: An ∞-topos with non-hypercomplete spheres
A type X is called ∞-connected if "every hole in X can be filled", meaning X and all its iterated identity types are merely inhabited. While any such X would be contractible in classical homotopy theory, this implication (called Whitehead's principle) can fail in homotopy type theory. We can recover it to an extent by working with hypercomplete types, those which "believe" all ∞-connected types are in fact trivial.
One might hope that this phenomenon of non-hypercompleteness only occurs with types that are somehow large or complicated. In this talk I will show this is not the case by describing a model of type theory in which the 2-sphere fails to be hypercomplete. I'll also discuss some implications for the independence of pushouts from other higher inductive types, following a suggestion of Andrew Swan.
Fabian Grubmüller: The Category of Iterative Sets in Cubical Agda
Iterative sets form a constructive Tarski-style universe V⁰ of h-sets that is itself an h-set. It arises naturally from the study of iterative multisets, where V⁰ is defined as a particular W-type for which the indexing function is restricted to embeddings. In previous work, Gratzer, Gylterud, Mörtberg, and Stenholm showed that V⁰ can be equipped with the structure of a Category with Families, that admits both Π- and Σ-structures. While their proofs were rather straightforward on paper, their Unimath Agda formalization faced significant obstacles, particularly for the Σ-structures.
In my master's thesis, I explored whether a formalization of this using Cubical Agda would be easier, which ultimately turned out not to be the case. In this talk, I will present the results and challenges of this effort as well as the continuing work together with Anders Mörtberg and Peter Lumsdaine.
Chaitanya Leena Subramaniam: Orthogonality calculi in enriched (∞-)categories and the small object argument (j.w.w. Mathieu Anel)
If E is an inner product space (a real vector space equipped with a bilinear, positive definite scalar product) and u is a vector in E of norm ≤ 1 (i.e. u is “small”), the projection operator from E onto the orthogonal complement of u can be computed using an iterative construction that bears a strong resemblance to the construction in category theory called the "small object argument" for weak factorisation systems.
If C is a category with all colimits and u is a suitably "small" morphism in C, the small object argument is an iterative construction that factors any morphism in C through an "orthogonal complement" of u.
The goal of this talk is to show that this analogy with ℝ-modules can be extended quite far. Let V be a locally presentable, closed symmetric monoidal category. The arrow category Arr(C) of any V-cocomplete V-category C has the structure of a free Arr(V)-module, where Arr(V) is equipped with the closed symmetric monoidal tensor product known as the “pushout-tensor". By adjointness, this module structure on Arr(C) equips Arr(C) with an enrichment over Arr(V) that is the analogue of an inner product for a vector space. This enrichment can be used to define various notions of orthogonality between morphisms of C.
We describe a general enriched small object argument, which is an iterative construction that computes a suitable projection operator associated to any of these notions of enriched orthogonality. In particular, several kinds of fibrations of cubical sets (indeed, of cubical presheaves valued in any n-topos) can be characterised using enriched orthogonality, and their associated weak factorisation systems can be constructed using the enriched small object argument.
This perspective extends to enriched ∞-categories, for any presentable, closed symmetric monoidal ∞-category V.