Stockholm–Göteborg joint type theory seminar
Time: Wed 2021-12-08 13.00 - 17.00
Location: SU, Kräftriket, Building 5, Room 32
Lecturer: Evan Cavallo, Brandon Doherty, Max Zeuner and Felix Cherubini
12:15–13:00 Lunch at Kräftan
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
14:45–15:30 Coffee break
15:30–16:15 Max Zeuner: Formalizing Affine Schemes in Cubical Agda
16:15–17:00 Felix Cherubini: More synthetic approaches to formalization
18:00 Dinner (location TBD)
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
Abstract: 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.
15:30–16:15, Max Zeuner, Formalizing Affine Schemes in Cubical Agda
Abstract: 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 joint work with Anders Mörtberg.
16:15–17:00, Felix Cherubini, More synthetic approaches to formalization
Abstract: 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.