The Department of Mathematics
Middlesex College
London, ON
Canada, N6A 5B7
Tel: 519.661.3639
Fax: 519.661.3610
Undergraduate inquiries:
math-inquiry@uwo.ca
Graduate inquiries:
math-grad-program@uwo.ca
All other inquiries:
mathdept@uwo.ca
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:
Date | Speaker | Talk information |
February 21 |
Simon Huber University of Gothenburg |
Homotopy canonicity for cubical type theory Cubical type theory provides a constructive justification of homotopy type theory and satisfies canonicity: every natural number is convertible to a numeral. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. In this talk I will present why if we remove these equations for the path lifting operation from the system, we still retain homotopy canonicity: every natural number is path equal to a numeral. The proof involves proof relevant computability predicates (also known as sconing) and doesn't involve a reduction relation. |
March 7 |
Evan Cavallo Carnegie Mellon University |
TBA TBA |
March 21 |
Dan Licata Wesleyan University |
TBA TBA |
April 4 |
Joachim Kock Universitat Autonoma de Barcelona |
TBA TBA |
April 18 |
Paolo Capriotti University of Nottingham |
TBA TBA |
May 2 |
Mathieu Anel Carnegie Mellon University |
TBA TBA |
May 16 |
Andrej Bauer University of Ljubljana |
TBA TBA |
Date | Speaker | Talk information |
February 7 |
Nima Rasekh MPI Bonn |
Algebraic Topology in an Elementary Higher Topos An elementary higher topos is a higher category which should sit at the intersection of three concepts: higher category theory, algebraic topology and homotopy type theory. The goal of this talk is to give concrete examples of these connections. |
January 31 |
Nicola Gambino University of Leeds |
From algebraic weak factorisation systems to models of type theory Algebraic weak factorisation systems are a refinement of the classical weak factorisation systems in which diagonal fillers are given by a prescribed algebraic structure. The notion of an algebraic weak factorisation system was introduced by Marco Grandis and Walter Tholen, and subsequently refined by Richard Garner, who then developed the theory in a series of joint papers with John Bourke. In this talk, I will explain general methods for constructing weak factorisation systems that can be used for defining models of dependent type theory satisfying all the required strictness conditions. This is based on joint work with Christian Sattler and subsequent work in the Leeds PhD thesis of Marco Larrea. Media: slides, no video. |
Date | Speaker | Talk information |
December 6 |
Eric Finster Inria - Rennes |
Towards Higher Universal Algebra in Type Theory I will propose a definition of "coherent cartesian polynomial monad" in type theory. Special cases of the proposal yield definitions of ∞-operads, ∞-categories and ∞-groupoids. In addition, I describe a definition of coherent algebra over such a monad, leading to a proposed internal description of objects such as En-types and diagrams of types valued in the universe. |
November 22 |
Floris van Doorn University of Pittsburgh
|
Towards Spectral Sequences for Homology
Spectral sequences form a powerful tool which can be used to compute homotopy, homology and cohomology groups of a wide variety of spaces. We have constructed two important spectral sequences in homotopy type theory, the Atiyah-Hirzebruch and Serre spectral sequences for cohomology. These spectral sequences have analogues for homology, but they have not been constructed in HoTT yet. However, many parts of our construction could be reused to construct the corresponding spectral sequences for homology.
In this talk I will introduce spectral sequences and review the spectral sequences we have constructed and some of their applications. Furthermore, I will describe what parts are still missing to construct the Atiyah-Hirzebruch and Serre spectral sequences for homology.
The construction of the spectral sequences for cohomology is joint work with Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Egbert Rijke and Mike Shulman.
|
November 8 |
Guillaume Brunerie Stockholm University |
Computer-generated proofs for the monoidal structure of the smash product The smash product is a very useful operation in algebraic topology and it can be defined in HoTT as a certain higher inductive type. One of its basic properties is the fact that it is a (1-coherent) monoidal product on pointed types, but proving this fact turns out to be very technical. I will present some work in progress aiming at proving it via some form of higher dimensional rewriting and meta-programming. The idea is to write an (untrusted) external program to generate a formal proof, which can then be formally checked by a proof assistant.
|
October 25 |
Nicolai Kraus University of Nottingham |
Some connections between open problems I will give an overview of my plan to construct connections between several unsolved questions. The following are important constructions that we would like to perform internally in type theory: |
October 11 |
Kuen-Bang Hou (Favonia) University of Minnesota |
Towards efficient cubical type theory Cubical type theory attracted much attention in the homotopy type theory community because it achieved canonicity in the presence of univalence and higher inductive types. To date, there are many variants of cubical type theory and experimental proof assistants based on them. |
September 27 |
Dimitris Tsementzis Rutgers University
|
First-Order Logic with Isomorphism First-order logic with isomorphism (“FOLiso”) is a formal system which relates to HoTT and the Univalent Foundations in a similar way that first-order logic with equality relates to ZFC and set-theoretic foundations. In particular, FOLiso gives a precise framework in which to study “first-order" theories defined on homotopy types (e.g. precategories, univalent categories), just as first-order logic with equality gives a precise framework in which to study first-order structures and theories defined on sets. I will first introduce the syntax and proof system of FOLiso as an extension of M. Makkai’s FOLDS. Then I will define a semantics for FOLiso in terms of homotopy types and describe a proof of soundness and completeness for this semantics. I will conclude by sketching applications in various directions. Media: video, slides. |
September 20 |
Andy Pitts University of Cambridge |
Axiomatizing Cubical Sets Models of Univalent Foundations |
Date | Speaker | Talk information |
May 24 |
Thierry Coquand University of Gothenburg |
A survey of constructive models of univalence |
May 10 |
Thorsten Altenkirch University of Nottingham |
Towards higher models and syntax of type theory
|
April 26 | Martín Hötzel Escardó
University of Birmingham |
Constructive mathematics in univalent type theory I want to share my experience of doing constructive mathematics in univalent type theory, compared to my previous experience in e.g. elementary-topos type theory (as in Lambek and Scott), Martin-Löf type theory, Bishop mathematics. |
April 12 |
Michael Shulman University of San Diego |
Type 2-theories Homotopy type theory is hypothesized to be an internal language for (∞,1)-toposes. However, recent developments suggest that more than this, what is needed is an internal language for collections of several (∞,1)-toposes together with functors between them, such as adjunctions, monads, comonads, non-cartesian monoidal structures, and so on. For instance, a cohesive (∞,1)-topos comes with an adjoint triple of two monads and a comonad, while a tangent (∞,1)-topos comes with a monad that is also a comonad and also a non-cartesian "smash product" monoidal structure. Just as ordinary homotopy type theory is a "doctrine" or "2-theory" for (∞,1)-toposes, each such situation should come with its own "2-theory": a dependent type theory with extra information characterizing the additional structure. But developing even one dependent type theory formally is a lot of work, so we would like a general framework and a general theorem that can then simply be specialized to all such 2-theories. I will sketch such a framework, which is under development in joint work with Dan Licata and Mitchell Riley. |
March 29 |
Ulrik Buchholtz Te chnische Universität Darmstadt |
From Higher Groups to Homotopy Surfaces Homotopy type theory can be seen as a synthetic theory of infinity groupoids. From this perspective, the pointed, connected types represent infinity groups. The elements are those of the loop space, and the operations on identity types provide the higher group structure.
In this talk, I'll explain what basic group theory looks like from this viewpoint. One aspect is that of categorifying ordinary group theory by using a univalent universe to present many groups. For example, the cyclic group on n elements is the loop space of the type of n-element sets equipped with a cyclic ordering.
In the second half of the talk, I'll focus on the 2-dimensional orthogonal group, and use this to talk about the homotopy types of surfaces.
The talk follows the synthetic approach to homotopy theory as developed in the HoTT book. Beyond that, a basic familiarity with ordinary group theory and the result on the classification of surfaces from topology will be helpful.
Some of the material will be from arXiv:1802.04315 (joint with Floris van Doorn and Egbert Rijke) and arXiv:1802.02191 (joint with Favonia), and some material is brand new.
|
March 15 |
Carlo Angiuli Carnegie Mellon University |
Computational semantics of Cartesian cubical type theory Dependent types are simultaneously a theory of constructive mathematics and a theory of computer programming: a proof of a proposition is at the same time a program that executes according to a specification. Homotopy type theory reveals a third aspect of dependent types, namely their role as an extensible formalism for reasoning synthetically about objects with homotopical structure. Unfortunately, axiomatic formulations of univalence and higher inductive types disrupt the computational character of type theory, which pivots on a property called canonicity. I will discuss Cartesian cubical type theory, a univalent type theory in which the canonicity property holds, based on a judgmental notion of cubes with diagonals, faces, and degeneracies, and uniform Kan operations that compute according to their types. I will consider it primarily through the lens of its computational semantics, defined using a cubical generalization of the technique of logical relations, which licenses reading proofs as programs. This talk is based on joint work with Favonia and Robert Harper, described in arXiv:1712.01800. Some familiarity with the syntax and rules of type theory will be very helpful; I will not assume knowledge about computational semantics or logical relations.
|
March 1 |
Emily Riehl Johns Hopkins University |
The synthetic theory of ∞-categories vs the synthetic theory of ∞-categories 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. |
February 15 |
Peter LeFanu Lumsdaine Stockholm University |
Inverse diagram models of type theory 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 C I 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 C I, 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 C I 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. |