Paolo Capriotti Darmstadt University of Technology

Globular Models of Type Theory

I will report on work in progress towards a constructive model of homotopy type theory based on simplicial objects in globular sets. The basic idea is as follows: I first use globular sets to build a model of a limited form of type theory without identity types, but equipped with a notion of "contractible type", corresponding to a certan class of trivial fibrations in the model. Then, I consider ∞-groupoid objects in this model, implemented as (groupoidal) complete Segal objects. Correctness of this construction is clear, because classically it can be performed in the opposite order, yielding locally constant globular spaces, which is an equivalent presentation of the ∞-category of spaces. When working in a constructive setting, the Segal conditions can be expressed as contractibility conditions, which are homotopically well behaved within globular sets. This allows us to work around the usual difficulties encountered in constructive formulations of the simplicial model of type theory.

Evan Cavallo Carnegie Mellon University

Cubical Indexed Inductive Types

Higher inductive types (HITs) provide a mutual generalization of inductive and quotient types and are an essential component of HoTT. However, the development of a general theory of HITs has lagged behind the use of specific instances; indeed, some examples employed in the HoTT book are still not known to have models in simplicial sets. I'll present my work with Robert Harper on giving a general schema for and computational interpretation of higher inductive types as part of a cubical type theory.

Our schema includes indexed inductive types, which are non-trivial in cubical type theory even without higher constructors. On the way, I'll discuss why cubical type theory is especially well-suited for practical reasoning with HITs, and which problems remain open in cubical and other settings.

Eric Finster University of Birmingham

The Cotopological Tower

Viewing type theory as an internal language for oo-topoi, the notion of a subtopos gets translated into that of a left exact modality.  In this talk, I will develop some of the basic theory of left exact modalities in type theory by providing both a recognition principle, as well as a means of generating them.  Furthermore, I will show how every left exact modality generates an infinite tower of associated modalities.  This tower is invisible to the theory of ordinary 1-topoi, and is therefore an entirely higher categorical phenomenon.  I will explain some properties of this tower, and how it may be viewed as an internalization of Goodwillie's Calculus of Functors.

Tslil Clingman Johns Hopkins University

Towards proof relevant category theory, as modelled by globular T-categories

In this talk we will aim to briefly outline the inadequacies of the classical presentations of (higher) categorical structures so as to motivate and clarify the notion of proof-relevance in analogy with the identity types in HoTT. We will then review general aspects of the theory of T-categories, as initiated by Burroni and continued by Leinster, before exploring a certain case which carries a compelling interpretation as a proof-relevant model of (higher) categories, the so-called definition L' of Leinster.

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.

Nicolai Kraus Eötvös Loránd University

Quotienting by Directed Relations

Quotients in MLTT were already studied by Hofmann (1995) and others. In HoTT, we can consider the higher inductive type A/R with constructors [_] : A -> A/R and e : R(x,y) -> [x]=[y], either as it is ("h-coequalizer") or its set-truncated version (the quotient). In a UIP-free setting, both versions come with difficulties: for the truncated version, it is unclear how to eliminate into general types, and the properties of the untruncated version are not well understood ("is the free group over a set again a set?").

I will talk about the connection between these problems, approaches to open questions, and solutions for special cases using a higher Seifert-van Kampen statement and a notion of directed relations.

This is joint work with Jakob von Raumer.

Paige North Ohio State University

Directed Weak Factorization Systems for Type Theory

In this talk, I report on progress to develop a directed homotopy type theory: a type theory with a 'hom' type former whose terms behave like morphisms or directed paths. The focus will be directed weak factorization systems, a variant of weak factorization systems which is better suited to capturing a notion of direction. I will then talk about how these model directed homotopy type theory.

Christian Sattler University of Gothenburg

Homotopy Canonicity

Because of the univalence and function extensionality axioms, homotopy type theory does not enjoy canonicity, a property expected from a constructive type theory. Voevodsky's 'homotopy canonicity' conjecture states that a homotopical version of this property still holds: every closed element of the natural number type is homotopic to a numeral. So far, this was known only for 1-truncated homotopy type theory, shown by Shulman using Artin glueing along a groupoid-valued global sections functor. In this talk, I will present a full proof of homotopy canonicity.

This is joint work with Krzysztof Kapulkin.

Andrew Swan University of Amsterdam

Separating Path Types and Identity Types

One of the interesting features of Cohen-Coquand-Huber-Mörtberg cubical type theory that distinguishes it from intensional Martin-Löf type theory is the presence of two distinct notions of equality: Path types and Id types. They are propositionally equivalent, but each satisfies certain definitional equalities that the other does not. I'll give an explanation why this distinction appears necessary in constructive mathematics when working with Orton-Pitts models of cubical type theory in presheaf categories.

Taichi Uemura University of Amsterdam

Cubical Assembly Models of Homotopy Type Theory

We present a model of homotopy type theory in the category of cubical assemblies (i.e. internal cubical objects in the category of assemblies) to combine homotopy type theory with the notion of realizability. We show some properties of this cubical assembly model compared to those of the ordinary assembly model of extensional type theory: it has a universe which is not only univalent but also impredicative in the sense that it is closed under dependent products over an arbitrary type; it does not satisfy the propositional resizing axiom with respect to the impredicative universe; it does not satisfy Church's Thesis, the axiom that all functions on the natural numbers are computable, but one can find a reflective subuniverse of cubical assemblies in which Church's Thesis holds.

This is joint work with Andrew Swan.

Liang Ze Wong University of Washington

A co-reflection of cubical sets into simplicial sets

Simplicial sets and cubical sets are two combinatorial models of homotopy types. I will introduce the categories of simplicial sets (sSet) and cubical sets with connections (cSet), and describe a co-reflective inclusion of sSet into cSet. This allows us to transfer any cofibrantly generated model structure in which cofibrations are monomorphisms from sSet to cSet, thus obtaining cubical analogues of the Quillen and Joyal model structures.

This is joint work with Krzysztof Kapulkin and Zachery Lindsey.