SPRING 2023 Program
Fridays 1-3pm in BH 150
January 20, Mathieu Anel — Smooth and proper objects for a fibration
I will show how ideas of dependent type theory (dependent sums and dependent products) can be used to revisit features of topology (locally contractible and compact spaces). I will present a general framework for dependent sums and dependent products, and apply it to study the fibration of etale maps over the category of topoi. We shall see that the morphisms of topoi along which this fibration has dependent sums are the locally contractible morphisms, and the morphisms along which dependent products exists are proper morphisms. This is jww Jonathan Weinberger.
January 27, Henrik Forssell — Locales of models and the definability theorem for coherent logic
In his PhD Thesis (Stockholm University), Johan Lindberg gave an explicit description of the Joyal-Tierney representation theorem in terms of locales of models of geometric theories. We revisit this description and show an example application of it by giving a constructive formulation and proof of the Definability Theorem for coherent logic (Elephant, D3.5.1).
Johan Lindberg's Thesis
February 3, Wentao Yang — Deligne's completeness theorem
Deligne's theorem states that any coherent topos has enough points. The theorem can be viewed as a completeness theorem when specialized to the classifying topos of a geometric theory. First we explain this connection to logic and then present a proof of Deligne's theorem.
February 10, Pietro Sabelli — Revisiting the equivalence between theories and models of dependent type theory using Curien’s explicit syntax
A good notion of semantics for a type theory calculus should give rise to an equivalence between theories and models through the syntactic category/internal language constructions. In the case of dependent type theory, Pierre Clairambault and Peter Dybjer proved in detail that Martin-Löf's type theories and locally cartesian closed categories are equivalent. There, the syntax is presented as a generalized algebraic theory. Motivated by the goal of finding suitable semantics for the intensional level of the Minimalist Foundation, I am working on a formalization in Agda of an analogous result using Curien’s explicit syntax. I will argue that this syntactical choice can give us insights into categorical semantics, in particular concerning the coherence problem.
February 17 (10am on Zoom), Eric Finster — The (∞,1)‑category of Types
A major outstanding difficulty in Homotopy Type Theory is the description of coherent higher algebraic structures. That is, well-behaved algebraic structures on types which are not assumed to be truncated. A classic example which motivates the desire to define such structures is the universe of type theory itself. Indeed, it is well known that the natural structure possessed by types and functions between them is not an 1-category, but rather an (∞,1)‑category. Expressing this fact appears to required principles which go beyond the standard presentation of MLTT.
In this talk, I will describe how the addition of a finite collection additional definitional equalities designed to render the notion of "opetopic type" definable in fact allows one to construct the (∞,1)‑category structure on the universe of types.
slides
February 24, Jonas Frey — « Seminar Surprise »
March 3, Andrew Swan — Oracle modalities
I give a new definition of function computable relative to an oracle, based on the classic result by Hyland that Turing degrees embed into the lattice of subtoposes of the effective topos. Higher modalities in homotopy type theory play a key role at every step. Justified by realizability semantics, we can assume that all functions N -> N are computable. In order to talk about functions that are not necessarily computable we use the modality of double negation sheafification. We think of functions in double negation sheaves, which we refer to as *oracles*, as external functions in sets that we can construct and reason about using classical logic. We say the *oracle modality* for an oracle is the smallest modality forcing the oracle to be total, and think of functions in the corresponding reflective subuniverse as computable relative to the oracle. By augmenting HoTT with certain axioms we can do some basic synthetic computability theory, including some reasoning about programs that use unbounded search using the new axiom of *Markov induction*. I also give a simple definition of homotopy group for a Turing degree and prove that two Turing degrees are equal as soon as they have isomorphic homotopy groups.
March 10, spring break — no seminar
March 13, 20, 27, Denis-Charles Cisinski, Hoang Kim Nguyen, Tashi Walde — Univalent Directed Type Theory
We will introduce a version of dependent type theory that is suitable to develop a synthetic theory of 1‑categories. The axioms are both a fragment and an extension of ordinary dependent type theory. The axioms are chosen so that (∞,1)‑category theory (under the form of quasi-categories or complete Segal spaces) gives a semantic interpretation, in a way which extends Voevodsky's interpretation of univalent dependent type theory in the homotopy theory of Kan complexes. More generally, using a slight generalization of Shulman's methods, we should be able to see that the theory of (∞,1)‑categories internally in any ∞‑topos (as developed by Martini and Wolf) is a semantic interpretation as well (hence so is parametrized higher category theory introduced by Barwick, Dotto, Glasman, Nardin and Shah). There are of course strong links with ∞‑cosmoi of Riehl and Verity as well as with cubical Hott (as strongly suggested by the work of Licata and Weaver), or simplicial Hott (as in the work of Buchholtz and Weinberger). We will explain the axioms in detail and have a glimpse at basic theorems and constructions in this context (Yoneda Lemma, Kan extensions, Localizations). We will also discuss the perspective of reflexivity: since the theory speaks of itself (through directed univalence), we can use it to justify new deduction rules that express the idea of working up to equivalence natively (e.g. we can produce a logic by rectifying the idea of having a locally cartesian type). In particular, this logic can be used to produce and study semantic interpretations of Hott.
Talk 1: video, slides intro, slides talk
Talk 2: video, slides
Talk 3: video, slides
March 24, Claymont retreat — no seminar
April 7, Astra Kolomatskaia Displayed Type Theory and Semi-simplical types
We introduce Displayed Type Theory (dTT), a multi-modal two-layered type theory whose outer layer consists of types with augmented semi-simplicial structure. The simplicial structure is exposed to the user via the fully computational parametric operation ᵈ (called display or dependency). The inner “discrete layer” represents the universe of homotopy type theory and conjecturally has semantics in any infinity-topos. It is possible to construct semi-simplicial types in the “simplicial layer” and subsequently to reflect them into the discrete layer via the fully computational modality ◇. Upon doing this, the definition of semi-simplicial types unfolds into infinitely many mutually recursive definition in the language of Book HoTT.
April 21, Greg Langmead Towards gauge theory in homotopy type theory
Gauge theory is the study of connections on smooth manifolds, and the solution set of functions defined on the space of connections. Sometimes these functions have terms coupling connections to sections of associated vector bundles, as in the standard model of particle physics. The starting point of gauge theory is the theory of principal bundles and their isomorphisms. I will remind us of the theory of higher groups in homotopy type theory and how we can think of deloopings as classifying spaces for principal bundles. I will show some related types that emerge from deloopings and which let us move around inside a space of symmetries, using identity types. Then I will show some work in progress to define connections and curvature using the modalities of real cohesion together with the delooping.
April 28, Owen Milner Formalizing the Whitehead tower in cubical agda
This talk will present details of a formalization, in cubical agda, of the key properties of the Whitehead tower. The material formalized includes the definition of the Whitehead tower, a proof of that its objects satisfy a universal property, the computation of their homotopy groups, and the identification of the fibers of the structure maps of the tower as particular Eilenberg-MacLane spaces.
May 5, Steve Awodey Cartesian cubical model categories
The category of Cartesian cubical sets is introduced and endowed with a Quillen model structure using ideas coming from recent constructions of cubical systems of univalent type theory.
Earlier seminars are listed here.