Department of Philosophy
Carnegie Mellon University
Pittsburgh, PA  15213

Office: Baker Hall 148

email :

main page

A view to mathematics


Pittsburgh's HoTT Seminar

The seminar Zroom

Meeting ID: 622 894 049
Fridays 1-3pm

Fall 2020 program

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 Agda formalization


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 arXiv:2009.05547.

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 Type Theory.
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.


Seminars of previous years


back to main page


all pictures are copyrighted