Homotopy Type Theory Electronic Seminar Talks is a series of research talks by leading experts in Homotopy Type Theory. The seminar is open to all, although familiarity with Homotopy Type Theory will be assumed. To attend a talk, please follow the instructions below.
We are using Zoom for the talks. Zoom is similar to Skype, and provides software for all common platforms and devices. Please install the software and make at least one test call before joining a talk. Please join the meeting a few minutes before the scheduled start time and mute your microphone when not asking a question. To join please follow the link:
We encourage attendees from the same institution to attend using one connection.
Electronic seminars are becoming more common in mathematics and you may be interested in attending some of them:
Johns Hopkins University
The synthetic theory of ∞-categories vs the synthetic theory of ∞-categories
Abstract: Homotopy type theory provides a “synthetic” framework that is suitable for developing the theory of mathematical objects with natively homotopical content. A famous example is given by (∞,1)-categories — aka “∞-categories” — which are categories given by a collection of objects, a homotopy type of arrows between each pair, and a weak composition law. In this talk we’ll compare two “synthetic” developments of the theory of ∞-categories — the first (joint with Verity) using 2-category theory and the second (joint with Shulman) using a simplicial augmentation of homotopy type theory due to Shulman — by considering in parallel their treatment of the theory of adjunctions between ∞-categories. Afterwards, I hope to launch a discussion about what considerations might motivate the use of homotopy type theory in place of classical approaches to prove theorems in similar settings.
Ideal background: some familiarity with notions of a (ordinary strict 1-)category, functor, natural transformation, and the definition of an adjunction involving a unit and a counit (just look these up on wikipedia). Plus standard type theory syntax and the intuitions from the Curry-Howard-Voevodsky correspondence. I’ll be talking about (∞,1)-categories but won’t assume familiarity with them.
Carnegie Mellon University
Computational semantics of Cartesian cubical type theory
Peter LeFanu Lumsdaine
Inverse diagram models of type theory
Abstract: Diagram models are a flexible tool for studying many logical systems: given a categorical model C and index category I, one hopes that the diagram category CI will again be a model.
For the case of intensional type theory, this becomes a little tricky. Since most logical constructors (e.g. Σ-types, Id-types) are not provably strictly functorial, it is difficult to lift them from structure on C to structure in CI, for arbitrary I.
However, in case I is an inverse category — roughly, something like the semi-simplicial category ΔI — this difficulty can be surmounted by taking the types of CI to be Reedy types, analogous to Reedy fibrations in homotopy theory.
I will discuss the construction of these models (and slightly more general homotopical diagram models) in the setting of categories with attributes, along with the application of these models to the “homotopy theory of type theories”.
The work of this talk is joint work with Chris Kapulkin, in arXiv:1610.00037 and a forthcoming companion article; see also Shulman arXiv:1203.3253 for a closely related construction.
A basic familiarity with categorical models of type theory will be helpful, i.e. categories with attributes or similar; see here for an introductory overview of these.