StockholmGoteborgMeeting211208
Stockholm–Göteborg meeting on Wednesday, 8 December 2021 in Stockholm and online
Program
| Time | Speaker | Title |
|---|---|---|
| lunch | ||
| 13:15–14:00 | Evan Cavallo | Another model structure presenting spaces from a cubical type theory |
| 14:00–14:45 | Brandon Doherty | Cubical models of higher categories |
| fika | ||
| 15:30–16:15 | Max Zeuner | Formalizing Affine Schemes in Cubical Agda |
| 16:15–17:00 | ||
| dinner |
Abstracts
Brandon Doherty — Cubical models of higher categories
We describe a new model structure on the category of cubical sets with connections whose cofibrations are the monomorphisms and whose fibrant objects are defined by the right lifting property with respect to inner open boxes, the cubical analogue of inner horns. We discuss the proof that this model structure is Quillen equivalent to the Joyal model structure on simplicial sets via the triangulation functor, and a new theory of cones in cubical sets which is used in this proof. We also introduce the homotopy category and mapping spaces of a fibrant cubical set, and characterize weak equivalences between fibrant cubical sets in terms of these concepts. This talk is based on joint work with Chris Kapulkin, Zachery Lindsey, and Christian Sattler, arXiv:2005.04853.
Max Zeuner — Formalizing Affine Schemes in Cubical Agda
Formalizing schemes has become somewhat of a benchmark problem for modern proof assistants and their mathematical libraries. In this talk we report on an ongoing project to formalize affine schemes in Cubical Agda, following a constructive approach due to Coquand, Lombardi and Schuster. We first describe the point-free construction of the Zariski lattice of a commutative ring that can already be found in the cubical library. We then sketch how working in a univalent setting allows one to construct the structure sheaf on the Zariski lattice in a way that more closely resembles the standard approach used in many classical textbooks, while also requiring additional coherence conditions that don't come up in other foundations. This is j.w.w. Anders Mörtberg.
Felix Cherubini — More synthetic approaches to formalization
Book-HoTT and cubical type theories provide the means for synthetic homotopy theory. It is also possible to treat other areas of pure mathematics synthetically. One prominent example are the Kock-Lawvere axioms of synthetic differential geometry. This talk will focus on a variation, which could be a basis for synthetic algebraic geometry, and its potential interaction with synthetic homotopy theory.