September 11, Steve Awodey
The equivariant model structure on cubical sets
The category of cubical sets has a model structure that can be described axiomatically in a way that is inspired by the model of type theory that it supports. Univalence, for example, plays a key role. This model category is not Quillen equivalent to the standard Kan one on simplicial sets, however. But there is another model structure taking the symmetries of the cubes into account, and that one is equivalent, according to a result by Christian Sattler. In this talk I will explain this more refined "equivariant model structure". Joint work with Thierry Coquand and Emily Riehl.
Slides of the talk
September 18, Thierry Coquand
Descent data operations and constructive sheaf models of type theory
This talk will present a higher generalisation of Lawvere-Tierney modalities
that appear naturally in the setting of constructive presheaf models of type theory
with univalence axiom and higher inductive types. Using the elementary and
essentially algebraic character of these models, they relativise to any
presheaf models over a base category. Any Grothendieck topology on this base
category gives then rise to a family of modal operations on types, that we can call
“descent data operations”. One main result is that these operations are left exact
modalities (and each universe of modal types is itself modal). Even in the case
of a trivial topology, the associated descent data operation may be non trivial
and defines a new internal model where equivalences are pointwise equivalences.
(This is closely connected to the recent use of the “cobar” operations by Mike Shulman.)
If time allows, we will end with some questions connected to an example where the base
site has already been used for an effective definition of the separable closure of a field
and for which we should be able to recover, in a constructive setting the cohomological
interpretation of the Brauer group of this field.
Notes of the talk
September 25, Jonathan Weinberger
Cocartesian fibrations in Simplicial Type Theory
In 2017, Riehl and Shulman introduced Simplicial Type Theory (STT) which is an extension of Homotopy Type Theory allowing to reason not only about infinity-groupoids, but infinity-categories.
A key gadget are judgmental extension types, based on ideas by Lumsdaine and Shulman, allowing for defining directed hom types.
The prime model is the infinity-topos of simplicial spaces, hence STT can be seen as a synthetic language for simplicial infinity-groupoids which allows for reasoning about infinity-categories interpreted as Rezk spaces.
We discuss aspects of the theory of cocartesian fibrations in this setting.
This is joint work with Ulrik Buchholtz.
Slides of the talk
October 2, Simon Henry
Left, right and weak model structures
Left semi-model structure, right semi-model structure and weak model structure are weakening of the notion of Quillen model structures that are still enough to formalize homotopy theory categorically, but are often easier to construct and enjoys better stability properties. I will review these notions, how they relates to each other and to other framework for categorical homotopy theory. This will include several recent or new results about construction of left, right and weak model structure that generalizes known results about Quillen model structure, and tends to be simpler.
Slides of the talk
October 9, Nicolai Kraus
Internal ∞-Categories with Families
It is natural to formalize the notion of a model of type theory (especially the syntax = intended initial model) inside type theory itself. This is often done by writing the definition of a category with families (CwF) as a generalized algebraic theory. What could be the success criterion from a HoTT point of view?
The typical first goal is that the initial model is an h-set or even has decidable equality. Our second goal is to make the "standard model" work, i.e. the universe U should be a CwF in a straightforward way (cf. Mike Shulman's 2014 question whether the n-th universe in HoTT models HoTT with n-1 universes). Unfortunately, it is hard to combine these two goals. If we include set-truncatedness explicitly in the definition of a CwF, then the "standard model" is not a CwF. If we don't, then the initial model is not an h-set.
The root of the problem is that 1-categories are not well-behaved concepts in an untruncated setting. The natural approach are higher categories, which corresponds to "equipping the syntax with all coherences" instead of truncating. In this talk, I will explain one approach to this based on a type-theoretic formulation of Segal spaces, expressed in HTS/2LTT. I will discuss what works and what is still open.
The talk will be based on arXiv:2009.01883.
October 16, Andrew Swan
The Nielsen-Schreier Theorem in Homotopy Type Theory
The Nielsen-Schreier theorem states that subgroups of free groups are themselves free groups. Although the statement of the theorem is simple, it is quite tricky to give a direct proof. However there is a conceptually clear proof using ideas from algebraic topology. This makes the Nielsen-Schreier theorem an ideal candidate for formalisation in homotopy type theory.
I will use the characterisation of groups in homotopy type theory as pointed connected 1 truncated types. Under this characterisation it is known that free groups are exactly wedges of circles and that subgroups correspond to pointed connected covering spaces (i.e. families of hSets indexed by the group). With these definitions the ideas of the algebraic topology proof can be applied directly. I will give a constructive proof of the special case of finite index subgroups and a proof of the full theorem using the axiom of choice. The finite index version has been verified electronically using Agda.
I will show the axiom of choice is necessary for the full theorem by giving an example of a boolean infinity topos where it is false. A related argument shows that the "untruncated" version of the theorem is provably false in HoTT even for finite index subgroups of finitely generated free groups.
Preprint arXiv:2010.01187 and
October 23, Denis-Charles Cisinski
The ∞-category of ∞-categories
This is a report on a joint work with Hoang Kim Nguyen which establishes a new way to construct the straightening/unstraightening correspondence in the context of quasi-categories.
October 30, Ivan Di Liberti
Formal Model Theory and Higher Topology
Motivated by the abstract study of semantics, we study the interaction between topoi, accessible categories with directed colimits and ionads. This theory amounts to a categorification of famous construction from general topology: the Scott topology on a poset and the adjunction between locales and topological spaces. This technology is then used in order to establish syntax-semantics dualities. Among the significant contributions, we provide a logical understanding of ionads that encompasses Makkai ultracategories.
Slides of the talk
November 6, Joachim Kock
Decomposition spaces, incidence algebras and Möbius inversion
I'll start rather leisurely with a review of incidence algebras
and Möbius inversion, starting with the classical Möbius function
in number theory, then incidence algebras and Möbius inversion
for locally finite posets (Rota) and monoids with the finite
decomposition property (Cartier-Foata), and finally their common
generalisation to Möbius categories (Leroux). From here I'll move
on to survey recent work with Gálvez and Tonks taking these
constructions into homotopy theory. On one hand we generalise
from categories to infinity-categories in the form of
Rezk-complete Segal spaces, taking an objective approach working
directly with coefficients in infinity-groupoids instead of
numbers. (Under certain finiteness conditions, numerical results
can be obtained by taking homotopy cardinality.) On the other
hand we show that the Segal condition is not needed for these
constructions: it can be replaced by a weaker exactness condition
formulated in terms of the active-inert factorisation system in
Delta. These new simplicial spaces we call decomposition spaces:
while the Segal condition expresses composition, the new
condition expresses decomposition. (An equivalent notion,
formulated in terms of triangulations of polygons, was discovered
independently by Dyckerhoff and Kapranov under the name unital
2-Segal space.) Many convolution algebras in combinatorics arise
as the incidence algebra of decomposition spaces which are not
categories, for example Schmitt's chromatic Hopf algebra of
graphs or the Butcher-Connes-Kreimer Hopf algebra of trees. The
Waldhausen S-construction of an abelian (or stable infinity-)
category is another example of a decomposition space; the
associated incidence algebras are versions of (derived) Hall
algebras. I will finish with some recent applications to free
probability (joint work with Ebrahimi-Fard, Foissy, and Patras).
November 13, Anders Mörtberg
Exceptional time: 10am-12pm (16:00-18:00 Europe)
Programming and proving with the structure identity principle
in Cubical Agda
One of the most striking consequences of univalence is the
structure identity principle (SIP) which states that equivalent
structured types are identifiable. There are multiple ways to
formalize this principle in homotopy type theory and I will discuss a
variation that we have recently formalized in Cubical Agda. The
constructive nature of cubical type theory allows us to reap the full
benefits of the SIP, making it possible to transport programs and
proofs along paths constructed using the SIP without losing
computation. We furthermore generalize the SIP to encompass also
relational representation independence results. By using higher
inductive types to simultaneously quotient two related implementation
types by a heterogeneous correspondence between them the
correspondence becomes an equivalence between the quotiented types,
thereby allowing us to obtain an equality of implementations by the
SIP. We have applied this to a wide variety of examples in the Cubical
Agda library, including algebraic structures, unary and binary
numbers, matrices, queues, and finite multisets.
This is joint work with Carlo Angiuli, Evan Cavallo and Max Zeuner.
Preprint can be found at
Slides of the talk
November 20, Tslil Clingman
More than merely composition: towards the theory of proof-relevant
categories and algebras
Homotopy Type Theory has profited immensely from the key insight that
precisely how two things are equal is important. This has, in some
areas, liberated the mathematician from the necessity of making choices
and performing the complex combinatorial computations of manipulating
presentations of objects and their equalities.
By analogy, in Category Theory many questions of coherence arise when we
are forced to choose a `the' composite for some given morphisms. One
approach to remedy these issues is by means of addressing composites by
their universal property. However, the theme of this talk is that such a
stance is not analogous to the key insight of Homotopy Type Theory.
Rather, as we will propose, the analogous view would entail that the
universal property of a composite ought to be data, and tracking
precisely how the universal property is implemented should be important.
To that end, in this talk we will introduce the idea of proof-relevant
categories and proof-relevant functors with the explicit aim of
capturing such data. The former objects are (potentially infinite
dimensional) category-like structures in which, for a given arrangement
of composable cells, there may be in general many proofs that the
arrangement interprets to another cell via composition. The latter
objects suitably generalise the anafunctors of Makkai to this setting:
on a given input, there may be in general many proofs that the functor
obtains a given value. We will strive to motivate these structures by
examples, and make connections to the univalent categories of Homotopy
These notions all emerge from the general framework of proof-relevant
algebras for globular T-categories. Time and interest allowing we will
examine how an arbitrary strict omega-category X may be combined with a
T-category A so that proof-relevant algebras over the result are
proof-relevant algebras for A with proof-relevant morphisms ``in the
shape of X''. From this point of view we will consider `compositions'
of proof-relevant functors as well as progress towards an appropriate
proof-relevant category of proof-relevant categories.
Slides of the talk
December 4, Colin Zwanziger
Sheaf Universes via Coalgebra
There is a well-known construction of a universe for presheaf models of type theory, which does not extend to arbitrary sheaf models (Hofmann and Streicher 1999).
This issue is naturally understood in the context of a framework such as natural models of type theory (Awodey 2012). We would like to leverage the fact that any sheaf topos arises as the category of algebras for a Cartesian reflector on a presheaf category. Unfortunately, it is not the case that natural models with universes are closed under the construction of algebras for the corresponding notion of Cartesian reflector (c.f. Coquand et al. 2020).
In my dissertation work, I show that natural models with universes are closed under the construction of *co*algebras for Cartesian comonads. This construction generalizes the presheaf case in a direction that includes many sheaf toposes.
I will focus in this talk on the example of sheaves on a topological space. We will use a coalgebraic presentation of sheaves. This is similar to the local homeomorphism presentation, but with the advantage that the inverse image of sheaves is strictly coherent (Marmolejo 1998). The natural model and universe structures can be described in relatively familiar terms.