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.

This is joint work with Thierry Coquand and Christian Sattler.

Evan Cavallo

Carnegie Mellon University

TBA

TBA

Dan Licata

Wesleyan University 

TBA

TBA

Joachim Kock

Universitat Autonoma de Barcelona

TBA

TBA

Paolo Capriotti

University of Nottingham

TBA

TBA

Mathieu Anel

Carnegie Mellon University

TBA

TBA

Andrej Bauer

University of Ljubljana

TBA

TBA

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.
In particular we show how every elementary higher topos has a natural number object, how this can be used to define truncations and how the existence of truncations implies the Blakers-Massey theorem.

Media: video, slides.

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.

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 E_n-types and diagrams of types valued in the universe.

I will report on progress towards formalizing the definition and suggest some constructions and applications making use of it. 

Media: video, slides.

Floris van Doorn

University of Pittsburgh

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.

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:
(1) a definition of semi-simplicial types;
(2) developing a theory of infinity-categories;
(3) homotopy type theory "eating itself";
(4) a "minimal/optimal" principle of eliminating truncations;
(5) showing that free higher groups over sets are sets, that the   suspension of a set is a 1-type, and variations/generalizations.

My expectation is that, in type theories where (1) can be solved (e.g.   HTS and 2LTT), the other problems can be solved as well. I will outline  the progress that various members of the HoTT community have made on  some of the questions. The emphasis of the talk will be on a framework  for quotienting by "directed" equivalence relations which I have  developed to attack problem (5), together with partial results and why  (5) is related to (1).

Media: video, slides.

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.

It may seem that the remaining task is to reconnect the syntax to standard models, but there are still numerous type-theoretic open problems arising from the concerns over efficiency and usability. In this talk, I will give an overview of several topics we are working on but not publicly presented before, including extension types, empty systems, the interplay between kinds and higher inductive types, and more!

Media: video, slides.

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.

(Most of the material is based on the preprint arXiv:1603.03092 with quite a few new additions based on ongoing work.)

Media: video, slides.

Andy Pitts

University of Cambridge

Axiomatizing Cubical Sets Models of Univalent Foundations

The constructive model of Homotopy Type Theory introduced by Cohen-Coquand-Huber-Mörtberg in 2015 (building on the work of Bezem-Coquand-Huber in 2013) uses a particular presheaf topos of cubical sets.  Since its introduction, much effort has been expended to analyse, simplify and generalize what makes this model of the univalence axiom tick, using a variety of techniques. In this talk I will describe an axiomatic approach -- the isolation of a few elementary axioms about an interval and a universe of fillable shapes that allow a univalent universe to be constructed. Not all the axioms are visible in the original work; and the axioms can be satisfied in toposes other than the original presheaf topos of cubical sets.  The axioms and constructions can almost be expressed in Extensional Martin-Löf Type Theory, except that the global nature of some of them leads to the use of a modal extension of that language.

This is joint work with Ian Orton, Dan Licata and Bas Spitters.

Media: video, slides.

Thierry Coquand

University of Gothenburg

  A survey of constructive models of univalence

I will try to survey what is known at this stage about constructive  models of univalence, and then some metatheoretical applications. Some of  these are: proof theoretic strength of the univalence axiom (with HITs), and   consistency of univalence with continuity principle and fan theorem, and  independence of the axiom of countable choice.

Media: video , slides.

Thorsten Altenkirch

University of Nottingham

Towards higher models and syntax of type theory

We (Ambrus Kaposi and myself) have defined the intrisic (no preterms) syntax of type theory in type theory using quotient inductive inductive types, that is set truncated higher inductive inductive types. Set truncation is necessary because we want to have decidability which we established using normalisation by evaluation. However, this stops us from defining any interesting semantic models, e.g. interpreting contexts as sets, types as families etc, because sets do not from a set (not for size reason but dimension). I suggest that we can overcome this problem by defining higher models of type theory and a higher syntax. I envisage that the higher syntax does form a set without being explicitely truncated, hence decability should still hold. In my talk I will describe the first steps towards this programme.

Media: video, slides.

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.
In doing so, I want to compare the old topological view of types and functions in constructive mathematics with the new homotopical view of equality in type theory.
There will be some new constructive theorems, too.

Media: video, slides.

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.

Media: video, slides.

Ulrik Buchholtz

Te chnische Universität Darmstadt

From Higher Groups to Homotopy Surfaces

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.

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.

Media: video,  slides.

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.

Media:  video, slides.