Date

Speaker

Talk information

Apr 16

Matthew Weaver

Princeton University

A constructive model of directed univalence in bicubical sets

Directed type theory is an analogue of homotopy type theory where types represent ∞-categories, generalizing groupoids. A bisimplicial approach to directed type theory, developed by Riehl and Shulman, is based on equipping each type with both a notion of path and a separate notion of directed morphism. In this setting, a directed analogue of the univalence axiom asserts that there is a universe of covariant discrete fibrations whose directed morphisms correspond to functions—a higher-categorical analogue of the category of sets and functions. In this talk, I’ll present a constructive model of a directed type theory with directed univalence in bicubical, rather than bisimplicial, sets. We formalize much of this model using Agda as the internal language of a 1-topos, following Orton and Pitts. First, building on the cubical techniques used to give computational models of homotopy type theory, we show that there is a universe of covariant discrete fibrations, with a partial directed univalence principle asserting that functions are a retract of morphisms in this universe. To complete this retraction into an equivalence, we refine the universe of covariant fibrations using the constructive sheaf models by Coquand and Ruch. (Joint work with Dan Licata.)

Media: video, slides.

Apr 2

Denis-Charles Cisinski

Universität Regensburg

Univalence of the universal coCartesian fibration

The model of higher categories given by Joyal's model structure for quasi-categories has univalent universes of coCartesian fibrations. This subsumes the existence of univalent universes of Kan fibrations proved by Voevodsky. Furthermore, the existence of such universes can be used as an alternative to the yoga of homotopy coherent nerves to prove all the essential features of higher category theory, giving a (directed) type theoretic approach to the foundations of higher categories.

Media: video, slides.

Mar 19

Jon Sterling

Carnegie Mellon University

Objective Metatheory of Dependent Type Theories

What type theorists and other researchers in type theory have in common is that they study theorems that hold of the initial model of type theory; but type theorists especially emphasize the theorems whose statements are sufficiently non-type-theoretic that they need not be preserved by homomorphisms of models. These theorems, sometimes called "metatheorems" or "admissibilities", are the means by which we conceive and justify computerized implementations of type theory, including canonicity, normalization, and decidability of type checking and judgmental equality.

The main tool for proving such theorems is Tait's method of computability, which has in the past several years been subject to a rapid campaign of rectification using the categorical language of Artin gluing. I will give an overview of this brave new "objective computability", emphasizing my recent joint work with Angiuli and Gratzer on a general gluing theorem for models of MLTT along flat functors into Grothendieck topoi, with an application to cubical type theory.

Media: video, slides.

Feb 20

 Karol Szumiło

University of Leeds

 The Constructive Kan-Quillen Model Structure

The classical Kan-Quillen model structure on the category of simplicial sets is a fundamental object in homotopy theory. Many proofs of its existence have been found, but (until recently) all of them relied on principles of classical logic: the law of excluded middle and the axiom of choice. For the purposes of interpretation of Homotopy Type Theory, such arguments were insufficient.

A fully constructive proof is possible, but it requires a careful adjustment of the definitions of cofibrations and weak homotopy equivalences of simplicial sets. In the talk, I will outline one such constructive argument, explaining how various standard techniques of simplicial homotopy theory need to be adapted to constructive logic.

This is joint work with Nicola Gambino and Christian Sattler, inspired by Simon Henry who was the first to obtain the result.

Media: video, slides.

Feb 6

Niels van der Weide

Radboud University

Constructing 1-Truncated Finitary Higher Inductive Types as Groupoid Quotients

In homotopy type theory, one can define spaces, such as the spheres and torus, with higher inductive types (HITs). These types generalize inductive types by allowing constructors for (possibly higher) paths beside constructors for points.

One scheme for HITs is defined by Dybjer and Moenclaey. It allows defining HITs by providing arities for constructors for the points, paths, and paths between paths. The arities are allowed to be recursive, but they have to be finitary.

In this talk, we show how to interpet the HITs defined by Dybjer and Moenclaey as 1-types using the grorupoid quotient. Concretely, this means we construct finitary 1-truncated HITs as groupoid quotients within type theory.

Media: video, slides.

Jan 23

Simon Henry

University of Ottawa

The language of a model category

Date

Speaker

Talk information

Dec 11,

4 PM Eastern

Richard Garner

Macquarie University

Polynomial comonads and comodules

To any locally cartesian closed category E one can associate a monoidal category Poly(E) of polynomials; it is (following von Glehn) the fibre over 1 of the free fibration with distributive sums and products on E, or equivalently (following Gambino and Kock) the category of polynomial endofunctors of E.

A result of Ahman and Uustalu shows that comonoids in Poly(E) (i.e., polynomial comonads) are the same as internal categories in E. It is then natural to ask: what is the bicategory of comonoids and bicomodules in Poly(E)? The goal of this talk is to explain the (slightly surprising) answer.

Media: video, slides.

Nov 20

Benno van den Berg

University of Amsterdam

Uniform Kan fibrations in simplicial sets

An important question in homotopy type theory is whether the existence of a model of univalent type theory in simplicial sets (and a model structure) can be proven constructively (say, in CZF with some inaccessibles). One approach would be to take the usual definition of a (trivial) Kan fibration as one's starting point and see how far one gets: this is the approach followed by Henry, Gambino, Szumilo and Sattler in recent work. It turns out that you can get quite far, but some issues remain (especially around the interpretation of Pi-types and coherence). Together with Eric Faber, I am pursuing a different approach in which we add uniformity conditions to the notion of a Kan fibration (as in the cubical sets model). The idea is that classically these conditions can always be satisfied, but not necessarily constructively. This has also been tried by Gambino and Sattler in earlier work, but in our view there are quite a few conditions missing in their definition of a uniform Kan fibration. In this talk, I will try to explain what our definition is, why we believe our definition is better (the idea is that we can prove, constructively, that it is "local"), and how far we are right now. 

Media: video, slides.

Nov 6

Andrew Swan

Carnegie Mellon University

Choice, Collection and Covering in Cubical Sets

In homotopical models of type theory such as cubical sets, propositional truncation has a rich structure. Instead of "identifying points," as in more traditional interpretations of extensional type theory in regular locally cartesian closed categories, one inductively adds new paths, while keeping existing points separate. This extra structure can be particularly clearly exposed by exploiting the fact that cubical sets are valid in a constructive metatheory, and assuming Brouwer's continuity principle, which is an anti-classical axiom stating that all functions from Baire space to the naturals are continuous. In this setting even very weak versions of the axiom of choice, such as WISC and a version of countable choice due to Escardo and Knapp, turn out to be false in the cubical set model. I will also talk about some very weak consequences of countable choice that are false in the model. This includes countable versions of collection and fullness from set theory (providing a solution to exercise 10.12 of the HoTT book). I will also talk about a couple of examples from homotopy theory: the product of countably many copies of the circle is not covered by any hSet and there are examples of hSets that are not covered by any constant cubical set.

Media: video, slides.

Oct 23

Anders Mörtberg

Stockholm University

Unifying Cubical Models of Homotopy Type Theory

(j.w.w. Evan Cavallo, Andrew Swan)

In recent years a wide variety of constructive cubical models of homotopy type theory have been developed. These models all provide constructive meaning to the univalence axiom and higher inductive types, but how are they related? In the talk I will give an answer to this question in the form of a generalization that covers most of the cubical models. The crucial idea of this generalization is to weaken the notion of fibration from the cartesian cubical set model so that it is not necessary to assume that the diagonal on the interval is a cofibration. This notion of fibration also gives rise to a model structure, generalizing earlier work on constructing model structures from cubical models of homotopy type theory.

Media: video, slides.

Oct 9

Andrej Bauer

University of Ljubljana

General type theories

There are many variants of dependent type theory, but it is difficult to find a complete and exact account of what a type theory is, as a formal system. We shall give a precise definition of what a type theory is in general, as a formal system whose components are various syntactic entities. The syntax of terms and types is described by a signature. Arbitrary inference rules are too unwieldy, so we next identify two properties that an acceptable rule must have. We similarly study what makes a family of rules into an acceptable type theory. To test the quality of our definition we prove fundamental meta-theorems about general type theories:

1. Presupposition theorem: if a judgement is derivable then so are its presuppositions.
2. Uniqueness of typing: if a term has type A and type B then A and B are judgmentally equal.
3. Elimination of substitution: every derivable judgement can be
derived without the substitution rule.

JOINT WORK WITH:
Philipp Haselwarter (University of Ljubljana)
Peter LeFanu Lumsdaine (Stockholm University)

Media: video, slides.

Mathieu Anel

Carnegie Mellon University

Descent v. Univalence

The purpose of the talk will be to explain the connection between the notion of descent, characteristic of infinity-topoi, and the notion of univalence, characteristic of homotopy type theory.

Media: video, slides.

Paolo Capriotti

Technische Universität Darmstadt

Polynomial monads as opetopic types

In a previous HoTTEST talk, Eric Finster presented a coinductive definition of polynomial monads that should make it possible to formulate higher algebra internally in HoTT. In my talk, I will show how one can connect Finster's construction to the formalism of opetopes and opetopic objects, and its connection with the Baez-Dolan construction for polynomial monads. More precisely, I will give a reformulation of Finster's definition of polynomial monad in terms of opetopic types satisfying a kind of Segal condition. It will turn out that, once the basic notion of trees over a polynomial is established, Finster's coherence for magmas can be expressed purely in terms of polynomials and their maps. This should hopefully provide a first step towards comparing Finster's definition with the established ∞-categorical notion of polynomial monad.

Media: video, "slides". 

 Joachim Kock

Universitat Autonoma de Barcelona

∞-operads as polynomial monads

I'll present a new model for ∞-operads, namely as analytic monads. This is joint work with David Gepner and Rune Haugseng. In the ∞-world (unlike what happens in the classical case), analytic functors are polynomial, and therefore the theory can be developed within the setting of polynomial functors. I'll talk about some of the features of this theory, trying to focus on aspects that might be of interest to type theory, in particular the construction of free monads, and the relevance of polynomial monads for the semantics of higher inductive types.

Media: video, "slides".

Dan Licata

Wesleyan University 

A Fibrational Framework for Substructural and Modal Dependent Type Theories (joint work with Mitchell Riley and Michael Shulman)

Modal type theory extends type theory with additional unary type constructors, representing functors, monads, and comonads of various sorts.  For example, the modalities discussed in the HoTT book are idempotent monads, while some recent extensions of HoTT make use of idempotent comonads.  Modal types can be used to speak synthetically about topology and geometry, and also have been used in the internal language semantics of cubical type theories. Over the past few years, we have been working on a general framework for modal type theories. In this framework, specific type theories can be specified by a signature---for example, "type theory with an idempotent monad and an idempotent comonad which are themselves adjoint".  Given a signature, instantiating general inference rules provides a syntax for working with the desired modal types.  While the framework does not automatically produce ``optimized'' inference rules for a particular modal discipline (where structural rules are as admissible as possible), it does provide a syntactic setting for investigating such issues, including a general equational theory governing the placement of structural rules in types and in terms.  While this is still work in progress, we hope to give a categorical semantics to the entire framework at once, saving the work of considering each modal type theory individually.

Media: video, slides.

 Evan Cavallo

Carnegie Mellon University

Internal Parametricity and Cubical Type Theory

A polymorphic function is intuitively said to be parametric when it behaves uniformly at all types. This concept was made precise by Reynolds, who defined parametric functions to be those with an action on relations and showed that all polymorphic functions definable in the simply-typed lambda-calculus are parametric. Recently, dependent type theories have been developed that internalize this property, which is known as parametricity; this work is closely connected to cubical type theory, both historically and methodologically. I'll discuss the similarities and differences between internally parametric and cubical type theory, the type theory we designed that combines the two, and potential applications to higher-dimensional theorem proving.

This is joint work with Robert Harper, and details can be found in our preprint arXiv:1901.00489.

Media: video, slides. 

 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.

Media: video, slides.

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

Technische 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.