HoTTEST Conference 2020
Homotopy Type Theory is a new area at the intersection of mathematics and computer science, combining ideas from several well-established fields: logic and type theory, homotopy theory, and formalization of mathematics.
The HoTTEST Conference of 2020 is a week-long online meeting, building on our series of HoTT Electronic Seminar Talks (HoTTEST). The conference will feature 10 talks by leading experts in the area. Familiarity with Homotopy Type Theory will be assumed.
The conference is open to all and no registration is required. To attend, follow the link
With speakers' permission, we will be posting their talks on our Youtube channel.
- Timothy Campion (University of Notre Dame)
- Eric Finster (University of Birmingham)
- Valery Isaev (Saint Petersburg Academic University)
- Peter LeFanu Lumsdaine (Stockholm University)
- David Jaz Myers (Johns Hopkins University)
- Paige Randall North (Ohio State University)
- Anja Petković (University of Ljubljana)
- Mitchell Riley (Wesleyan University)
- Michael Shulman (University of San Diego)
- Taichi Uemura (University of Amsterdam)
|Time \ Date
Titles and Abstracts
- Timothy Campion
- Eric Finster Weak Structures from Strict Ones
I will describe a technique for defining various weak higher structures by extending type theory with a universe of strict polynomial monads. Furthermore, I will describe implementation of the proposed theory in Agda using rewrite rules.
- Valery Isaev Indexed Type Theories
Indexed type theory is a version of homotopy type theory which represents indexed ∞-categories. It has two levels of types: the first level correspond to ordinary homotopy type theory and the second one represents indexed objects. Indexed type theories generalize other similar two-level systems such as a form of cohesive homotopy type theory and certain linear dependent type theories. It can be used to reason directly in ∞-categories which do not have all the structure required by homotopy type theory.
In this talk, I define indexed type theory and describe various constructions in it including finite and infinite (co)limits and object classifiers. I will give several examples of models of indexed type theory including spectra and quasicategories. I will also prove a special case of the indexed adjoint functor theorem using the language of indexed type theories.
- Peter LeFanu Lumsdaine
- David Jaz Myers Higher Scheier Theory
In a 1926 article, Otto Schreier gave a classification of all extensions of a group G by a (non-abelian) group K. This classification of extensions has come to be known as Schreier theory, and has been reformulated many times by many authors since. Just as central extensions by an abelian group are classified by group cohomology in degree 2, Schreier theory can be seen as an example of a classification by non-abelian group cohomology.
Higher Schreier theory concerns the classification of extensions of higher groups. Breen has generalized Schreier theory to sheaves of 2-groups. In this talk, we will give a proof of Schreier theory for oo-groups in homotopy type theory - and therefore for sheaves of ∞-groups by interpreting in various oo-toposes. Our main theorem is:
Let G and K be ∞-groups. Then the type of extensions of G by K is equivalent to the type of actions of G on the delooping BK.
One can immediately see the resemblence of this formulation of higher Schreier theory to the classification of split extensions of G by K by the homomorphic actions of G on K. We can derive this classification, and some others, as an immediate corollary.
We will also discuss the notion of central extensions, and navigate some subtleties concerning the notion of centrality for higher groups.
- Paige Randall North A Higher Structure Identity Principle
The Structure Identity Principle (SIP) is an informal principle asserting that isomorphic structures are equal. In univalent foundations, the SIP can be formally stated and proved for a variety of mathematical structures. This means that any statement that can be expressed in univalent foundations is invariant under isomorphism, or, put differently, that only structural properties can be stated in univalent foundations.
The SIP only applies to objects that naturally form a 1-category. In this talk, I will discuss a Higher Structure Identity Principle in univalent foundations for structures that naturally form a higher category (e.g., categories themselves).
This is joint work with Benedikt Ahrens, Mike Shulman, and Dimitris Tsementzis.
- Anja Petković Equality checking for Finitary type theories
Equality checking algorithms are essential components of proof assistants based on type theories, since they free users from the burden of proving judgemental equalities, and provide computation-by-normalization engines. Indeed, the type theories found in the most popular proof assistants are designed to provide such algorithms.
However, in a proof assistant that supports arbitrary user-definable theories, such as Andromeda 2, there may not be an equality checking algorithm available in general.
I will discuss the design of a user-extensible judgemental equality checking algorithm for finitary type theories that supports computation rules and extensionality rules. The user needs only provide the equality rules they wish to use, after which the algorithm devises an appropriate notion of normal form. We will also take a peek at how the implementation of the equality checking algorithm is used in the Andromeda 2 prover.
- Mitchell Riley Synthetic Spectra via a Monadic and Comonadic Modality
"Spectra" are the central objects of study in stable homotopy theory, and it is easy to define them internally in HoTT as Ω-spectra: a spectrum is a sequence of types with an equivalence between each type and the loop-space of the next. Working with these spectra in type theory can be quite difficult, however. In this talk we describe an extension of HoTT intended to be modeled in the category of "parameterised spectra", where a modality is used to identify the types that correspond to individual spectra. A pair of axioms are considered that internalise some features of the intended model, and which fix the "homotopy groups" (appropriately defined) of the sphere spectrum to be the stable homotopy groups of the ordinary higher inductive spheres.
- Michael Shulman Type-theoretic model toposes
Starting with the Awodey-Warren interpretation of identity types by path objects and Voevodsky's model of univalence in simplicial sets, various kinds of Quillen model categories have been used to interpret homotopy type theory. A "type-theoretic model topos" is a Quillen model category that is optimal for this purpose in many respects. On one hand, it has sufficient structure to interpret essentially all of "Book" HoTT, including in strict univalent universes and most higher inductive types. On the other hand, it is sufficiently general that any Rezk-Lurie-Grothendieck (∞,1)-topos can be presented by a type-theoretic model topos. This talk will sketch the definition of type-theoretic model topos and the proofs of these facts, including some variations of the definition that apply to models of cubical type theory.
- Taichi Uemura Abstract type theories
Many variants of dependent type theory admit the semantics based on categories with families (CwFs). I introduce an abstract notion of a type theory to give a unified account of the CwF-semantics of type theory. The key idea is to regard a CwF-model of a type theory as a functor to a presheaf category preserving certain structures. Basic results in the semantics of type theory are then stated and proved in a purely categorical way. In this talk I will explain motivations and intuitions behind my definition of a type theory.