Schedule
All talks will be in Baker Hall room A51: see the conference map.
| Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | |
|---|---|---|---|---|---|---|
| 9:30 | Registration | Pitts | Licata | Szumilo | Sattler | Buchholtz |
| 10:00 | Riehl | |||||
| 10:30 | Shulman | Weinberger | Stenzel | Sterling | Subramaniam | |
| 11:00 | Break | Break | Break | Break | Break | Break |
| 11:30 | Awodey | Christensen | Sestini | van den Berg | Finster | Joyal * |
| 12:00 | Coquand | Karnick | Weaver | Gambino | Brunerie | |
| 12:30 | Lunch | Lunch | Group Photo and Lunch | Lunch | Lunch | Lunch |
| 2:00 | Mörtberg | Rijke | Excursions | Zwanziger | Uemura † | End |
| 2:30 | Swan | North | Myers | Bidlingmaier | ||
| 3:00 | Francese | Rose | Cicala | Lo Monaco | ||
| 3:30 | Break | Break | Break | Break | ||
| 4:00 | Choudhury | Sozeau | Lessard | Moeneclaey | ||
| 4:30 | Cagne | Lynge | White | Bentzen | ||
| 5:00 | Helfer | Acosta | ||||
| 5:30 | Reception | |||||
| 6:00 | Dinner |
Titles and Abstracts
Ernesto Acosta: Calculational HoTT [slides]
Based on a loose correspondence between, on one hand, a first order version of intuitionistic logic with preeminence of equality and equivalence over implication, and on the other hand, homotopic equivalence properties of identity, Π, Σ and coproduct types, we formally restate homotopic type theory (HoTT) with equality and homotopic equivalence playing a preeminent role. In addition to this, we exhibit a calculational way of writing effective and elegant formal proofs based on appropriate notations and formats, as well as algebraic identities and inference rules involving the homotopic equivalences with which we restate HoTT.
Steve Awodey: A Quillen model structure on the category of cartesian cubical sets [slides]
We axiomatize the construction of a Quillen model structure on cubical sets, using ideas derived from recent constructions of models of cubical type theory. Some of these ideas are apparently new to homotopical algebra. The construction applies to cartesian cubical sets, as well as to the equivariant cubical model structure developed in recent joint work with Cavallo, Coquand, Riehl and Sattler.
Bruno Bentzen: Informal cubical type theory [slides]
Higher-dimensional type-theoretic foundations is gaining wider acceptance in the mathematical community since the emergence of homotopy type theory. One of the reasons can be attributed to the collective efforts of the authors of the book homotopy type theory to develop an informal but rigorous style of doing mathematics in natural language assuming higher-dimensional type theory as the underlying foundation. This ‘informal type theory’ project, originally proposed by Peter Aczel, was carried out in the book for an augmentation of intensional Martin-Löf type theory with the univalence axiom and higher-inductive types.
The aim of this talk is to propose a way of doing informal type theory with cubical type theory as the underlying foundation instead or, simply put, to present a cubical variant of the informal type theory project. This work is based on cartesian cubical type theory. We confine our talk to the introduction of an informal semantics for cubical type theory and its basic operations, and the development of a few informal proofs by adopting cubical methods as the implicit basis of our informal reasoning.
Martin Bidlingmaier: Coherence via big categories with families of locally cartesian closed categories [slides]
Locally cartesian closed (lcc) categories are natural categorical models of dependent type theory (Seely 1984). However, there is a slight mismatch: syntactic substitution is functorial and commutes strictly with type formers, whereas pullback is generally only pseudo-functorial and preserves universal objects only up to isomorphism. In response to this problem, several notions of models with strict pullback operations have been introduced, e.g. categories with families (cwf) (Dybjer 1995), and coherence techniques have been developed to strictify weak models such as lcc categories and obtain models with functorial substitution (Curien 2014, Lumsdaine and Warren 2015). While an interpretation of almost all of homotopy type theory is known to exist in arbitrary infinity toposes (Shulman 2019), even an interpretation of just intensional dependent type theory in arbitrary lcc quasi-categories is only conjectured (Kapulkin 2017).
This talk introduces the big cwfs of lcc 1-categories and lcc quasi-categories, a novel coherence construction for dependent type theories. In the 1-categorical case, the technique provides a new proof of the interpretation of extensional type theory in lcc categories. The big cwf of lcc quasi-categories supports substitution-stable type and term formers for dependent sums and products, but expected judgemental laws such as β equality hold only up to contractible path equality. I expect that this structure suffices to interpret a hypothetical weak variant of intensional type theory.
Our point of departure is the observation that, when working in type theory, changing the ambient context is akin to changing the base terms of the underlying theory. For example, proving v : σ ⊢ t : τ is equivalent to proving ⊢ t : τ in a type theory that was freely extended by a term v of type σ. We take the idea that contexts represent different type theories literally and assign to each context a separate model, i.e. a separate lcc category. Context extension then corresponds to freely adjoining an interpretation of a term to an lcc category.
Theorem: The big cwf of lcc 1-categories contains every lcc category up to equivalence, it has an initial context and comprehensions, and it supports Σ, Π and extensional Eq types.
This theorem enables the interpretation of a type theory with the corresponding features in (slices of) the big cwf. In the 1-categorical case, the existence of a context equivalent to a given lcc category C follows from the 2-monadicity of the category of strict lcc categories over the (2,1)-category of categories (Blackwell 1989). Roughly speaking, the context is obtained from C by forgetting about the canonical choice of lcc structure and adjoining a new one. it can thus be seen as a destrictification of C. For example, even when C happens to be equipped with a strictly functorial choice of pullback functors, the canonical pullback functors of the corresponding context will not have this property.
Guillaume Brunerie: A formalization of the initiality conjecture in Agda [slides]
The initiality conjecture, stating that the term model of type theory is initial in the category of models, is a well-known open problem about categorical semantics of type theory. The main obstacles to proving it are that it is very technical, and that it isn’t even clear what the precise statement should be. We present here a proof of the initiality conjecture for a specific version of Martin-Löf type theory. The proof is formally checked in Agda and can be extended by additional type/term-formers if needed.
Ulrik Buchholtz: Musings about 2-groups
I’ll talk about the beginnings of the theory of 2-groups in homotopy type theory. The basic definitions are very elegantly expressed in this setting, and many indeed appeared already in previous work with Floris van Doorn and Egbert Rijke. For instance, a 2-group is defined as a pointed, connected 2-type. Here I’ll discuss how to connect these abstract definitions with more traditional models in terms of crossed modules. Topics include the geometric realizations of crossed modules and butterflies in terms of gerbes, non-abelian cohomology, the Galois theory of 2-covering spaces, the Postnikov invariant, and Whitehead products for braided 2-groups.
Pierre Cagne: Identity types as equality predicates [slides]
Lawvere’s hyperdoctrines give a natural framework for interpreting first-order logic. Hyperdoctrines are bifibrations p:E→B whose fibers and itself satisfy nice properties reflecting the structure of first-order logic. The objects of the category B are meant to be the contexts of the logic while its morphisms are the terms. The objects of the category E are to be understood as predicates over contexts and the morphisms in each fiber is the entailment from one predicate to another. A key feature of an hyperdoctrine is the existence of binary products in B and terminal objects in the fibers of p that allow for a meaningful interpretation of the equality predicate: given an object A in B, the terminal predicate 1A over A can be pushed along the diagonal map A→A×A to produce a predicate EqA over A×A. This predicate satisfies the universal property expected from an equality relation, namely it is the smallest reflexive relation on A. This framework can be easily extended to interpret higher-order logic with extensional equalities.
On the other hand, the identity types of Martin-Löf’s intensional type theory find a natural semantics as path spaces in Quillen model categories, or refinements of such like Joyal’s tribes or Shulman’s type-theoretic fibration categories. Such a path space for a type A is obtained by factorizing the diagonal map A→A×A into a trivial cofibration followed by a fibration. There are uncanny similarities between the properties of this construction and the properties of equality predicates, yet they don’t fit in a common language.
The goal of this talk is to provide a first step toward the unification of hyperdoctrines with homotopical models of HoTT in a same framework. This is done by introducing relative weak/strong factorization system: these are the data of a functor p:E→B together with two classes of maps on E and two classes of maps on B satisfying lifting properties. In particular, classical weak/strong factorization systems on E are retrieved as the ones relative to E→1. We then prove that Grothendieck fibrations can be expressed as peculiar relative strong factorization system while fibrations in a tribe give rise to a peculiar relative weak factorization system. Relative factorization systems make it thus possible to define path spaces in the same fashion as equality predicates, providing a track to define more general model of intensional type theory.
Vikraman Choudhury: The finite-multiset construction in HoTT [slides]
We study the finite-multiset construction in HoTT as the free commutative monoid on a set (0-type).
Various formalisations of the finite-multiset construction, using 1-HITs and set quotients, will be presented and the computational content of their equivalence, stemming from the universal property, will be discussed.
Different approaches to characterising the path space of the finite-multiset construction of a set will be considered. They hinge on a lightweight decomposition of permutations as compositions of transpositions that arises from the commutation relation of creation/annihilation operators associated to the finite-multiset construction [4].
Our development provides all the necessary structural properties of the finite-multiset construction that further allow the formalisation of the relational model of differential linear logic [2] constructively.
The results are formalised in cubical Agda.
This is groundwork for applications to, on the one hand, the denotational semantics of a reversible programming language with finite types [1], and, on the other hand, the formalization of the free symmetric-monoidal completion of a groupoid (1-type) for developing the calculus of generalised species of structures [6,3] between groupoids and its application to higher-dimensional algebra [5].
This is joint work with Marcelo Fiore.
References
[1] J Carette, C-H Chen, V Choudhury, A Sabry. From reversible programs to univalent universes and back. In MFPS XIII, ENTCS 336, pages 5-25, 2018.
[2] T Ehrhard. An introduction to Differential Linear Logic: proof-nets, models and antiderivatives. In arXiv:1606.01642, 2016.
[3] M Fiore. Mathematical models of computational and combinatorial structures. In FOSSACS 2005, LNCS 3441, pages 25-46. Springer-Verlag, 2005.
[4] M Fiore. An axiomatics and a combinatorial model of creation/annihilation operators. In arXiv:1506.06402, 2015.
[5] M Fiore. An algebraic combinatorial approach to opetopic structure. Seminar on Higher Structures https://www.mpim-bonn.mpg.de/node/6586, MPIM (Bonn), 2016.
[6] M Fiore, N Gambino, M Hyland, and G Winskel. The cartesian closed bicategory of generalised species of structures. J. London Math. Soc., 77:203-220, 2008.
Dan Christensen: Localization at a prime in homotopy type theory [slides]
This talk will present results about localization at a prime in homotopy type theory. The main result is that for a pointed, simply connected type X, the natural map from X to its p-localization induces algebraic localizations on all homotopy groups. In order to prove this, I’ll describe new results about general reflective subuniverses and their separated types, including the fact that the separated types form a reflective subuniverse. As key steps towards proving the main theorem, I’ll explain how localization at a prime commutes with taking loop spaces for a pointed, simply connected type, and explicitly describe the localization of an Eilenberg-Mac Lane space K(G,n) with G abelian. This is joint work with Morgan Opie, Egbert Rijke and Luis Scoccola.
Daniel Cicala: The Borsuk-Ulam Theorem in Real-Cohesive Homotopy Type Theory [slides]
Real-cohesive homotopy type theory is an extension of homotopy type theory obtained by adding a string of modalities ʃ ⊣ ♭ ⊣ ♯ to encode Lawvere’s axiomatic cohesion. The ʃ modality compares higher inductive types with their set-theoretic counterparts, e.g. the circle as a 0-type base and 1-type loop : base → base and the circle as a set { (x,y) ❘ x,y ∈ R and x2+y2=1 }. The ♭ modality allows for non-continuous constructions, such as choosing the fixed point in the proof of Brower’s fixed point theorem. In this talk, we extend the use-case for real-cohesive homotopy type theory by importing a HoTT version of the classic Borsuk-Ulam theorem.
Thierry Coquand: Some constructive models of univalent type theory [slides]
I would like to first present ongoing work (with Steve Awodey, Evan Cavallo, Emily Riehl and Christian Sattler) on a refined notion of cartesian cubical sets. For this notion, we can show in a classical metatheory that the (-1)-types are the Booleans and the 0-types are the sets. I will then try to explain a possible application of such constructive models of univalence. If we relativize what we have done to presheaf models, we get directly a model of type theory and a model structure on cubical presheaves, which is obtained from a constructive model of univalent type theory (as explained in Steve’s talk). The (-1)-types (resp. 0-types) for this model are not the sieves (resp. ordinary presheaves) but they become them (in a classical metatheory) if we apply a suitable left exact modality.
Eric Finster: Coherent Polynomial Monads and Their Algebras
I will report on recent progress in defining and manipulating higher coherent structures in type theory via the introduction of coherent polynomial monads and their algebras. Possible topics include: the construction of simplicial types, a description of the monadic structure of the universe, and recognition principles for loop spaces. In addition to surveying the current state of affairs, I will suggest possible directions and applications of the theory.
James Francese: Toward a Homotopy Tripos for Higher Realizability [slides]
The syntactic side of tripos theory is somewhat less explored than that of toposes, especially when it comes to typed and higher-typed lambda calculi and other type theories. Yet it is meaningful to seek a notion of “tripos” with respect to these richer computational settings, especially for the sake of promoting the notion of realizability topos to a higher-categorical setting. This latter goal is desirable for many reasons, one of them being giving a computational interpretation of univalence in homotopy type theory, a problem for which there are currently several serious frameworks, e.g. [1, 5, 3]. The task of this talk will be to suggest the relevance of higher realizability to the prospect of a fully univalent computability theory and discuss a path toward a concrete definition of realizability infinity-toposes. In developing this definition, there is first a “naïve” approach which we will set aside, and then a more lengthy approach which begins not with the typical machinery of realizability toposes themselves, but with the higher categorification of Longo and Moggi’s notion of Turing category introduced in [6] and more lately discussed by Cockett and Hofstra in [2]. This frees us from some of the properties assumed in the Giraud-style definition of realizability toposes recently given by Frey in [4], and lets us pursue a theory of partitioned assemblies from scratch by first correctly understanding Turing objects in higher categories, which classically (i.e., 1-categorically) do yield realizability triposes since 1-categorical Turing objects are partial combinatory algebras. This approach also addresses issues with the newly introduced “cubical assemblies” in [7]; these yield realizability models with some higher dimensional features, but do not present a (higher) categorification of the classical realizability topos.
References
[1] C. Angiuli, H. Kuen-Bang (Favonia), R. Harper. “Cartesian Cubical Computational Type Theory: A Constructive Formulation of Two-Level Type Theory”. January 2018.
[2] J.R.B. Cockett, P.J.W. Hofstra. “Introduction to Turing Categories”. Annals of Pure and Applied Logic Volume 156, Issues 2–3, December 2008, Pages 183-209.
[3] C. Cohen, T. Coquand, S. Huber, and A. Mörtberg. “Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom”. 21st International Conference on Types for Proofs and Programs (TYPES 2015), 2018.
[4] J. Frey. “Characterizing partitioned assemblies and realizability toposes”. 2018, to appear in JPAA.
[5] S. Huber. “A Model of Type Theory in Cubical Sets”. Licentiate thesis, University of Gothenburg, May 2015.
[6] G. Longo and E. Moggi. “Gödel numberings, principal morphisms, combinatory algebras”. In Chytil and Koubek, editors, Mathematical Structures in Computer Science, volume 176 of LNCS, pages 397–406, Prague, 1984. Springer Verlag.
[7] T. Uemura. “Cubical Assemblies and the Independence of the Propositional Resizing Axiom”. Preprint, 2018. arxiv. abs/1803.06649
Nicola Gambino: Towards a constructive simplicial model of univalent foundations [slides]
We provide a partial solution to the problem of defining a constructive version of Voevodsky’s simplicial model of univalent foundations. For this, we prove constructive counterparts of the necessary results of simplicial homotopy theory, building on the constructive version of the Kan-Quillen model structure established by the second-named author. In particular, we show that dependent products along fibrations with cofibrant domains preserve fibrations, establish the weak equivalence extension property for weak equivalences between fibrations with cofibrant domain and define a univalent classifying fibration for small fibrations between bifibrant objects. These results allow us to define a comprehension category supporting identity types, Σ-types, Π-types and a univalent universe, leaving only a coherence question to be addressed.
Joseph Helfer: 2-categorical structures in Grothendieck fibrations and first-order homotopical logic [slides]
This work begins with the observation that the Voevodsky-Awodey-Warren-Kapulkin-Lumsdaine homotopical semantics for type theory can also be used to give a very simple semantics for (intuitionistic) first-order logic. We give a “functorial” formulation of the semantics using the framework of structured Grothendieck fibrations, by showing that for (suitable) model categories C, the fibration obtained by taking the fiberwise-homotopy-category of the codomain fibration over C has the structure needed to interpret intuitionistic first-order logic. We then prove an abstract result about such structured fibrations which implies a “homotopy-invariance” property for the homotopical semantics. To do this, we must make sense of the notion “homotopy-equivalent structures” – which, in the case of interest, corresponds to “pseudo-naturally isomorphic functors into the 2-category of spaces” – in the general context of the “fibrational semantics”. Hence, we show that the base category of a fibration (satisfying certain mild assumptions) automatically carries a 2-categorical structure – the 2-cells between f and g being “proofs (in the sense of the fibration) that f and g are equal” – which in the case of interest recovers the usual 2-category of spaces.
André Joyal: Problems and conjectures on polynomial functors and monads in ∞-toposes
The theory of polynomial functors and monads has applications to type theory and to the theory of operads. The theory was recently extended to polynomial functors in the category of spaces by Gepner, Haugseng and Kock. We conjecture that the (∞,2)-category of polynomial functors (in any ∞-topos) is cartesian closed (extending a result of Fiore, Gambino, Hyland and Winskel).The evidence depends on ideas from type theory (Awodey, Fiore). We also conjecture that the ∞-category of bimodules between polynomial monads (in any ∞-topos) is cartesian closed (extending a result of Gambino and J). The conjectures can be understood in terms of a conjectural 2-algebraic geometry. There is a connection with Goodwillie’s calculus.
Nachiket Karnick: The encode-decode method and higher group actions
The encode-decode method is a useful proof method used in Homotopy Type Theory, most notably in giving a more type-theoretic way of calculating the fundamental group of a circle (Licata-Shulman). In this talk we explore this method and what it means mathematically in terms of group actions. Understanding the homotopy groups of CW complexes is a higher dimensional analogue of the “word problem” in ordinary group theory, and the main technique used to solve the word problem is to give a free action of the group on something. I will talk about how this helps us to understand the loop space of a higher inductive type (particularly spheres) by giving a free and transitive (higher) group action (Buchholtz-van Doorn-Rijke) of this loop space on a type X. We then see how the definition of such an action relates to the encode-decode method. Finally, we will see how the encode-decode method can be used to calculate higher homotopy groups of spheres, in particular π3(S2) (joint work with Noah Snyder and Jacob Prinz).
Paul Lessard: Weak Z-Categories: Spectra and Symmetric Monoidal Higher Categories with a View Towards Dependent Linear Type Theory
First we describe an essentially algebraic theory, ΘZ, for Z-categories, a notion of higher category wherein all entities are morphisms between lower morphisms. We show that the model category induced by the test model structure on cellular sets induces a model structure on presheaves on ΘZ which presents weak Z-groupoids. We will then see that subcategory of pointed objects in this presheaf topos satisfying a finiteness condition present the (∞,1) category of spectra.
We will then relate the stable homotopy hypothesis that puts connective spectra as equivalent to picard ∞-groupoids to this presentation of spectra by observing that pointed Z-categories come equipped with a canonical monoidal structure.
We will observe that this structure is an avatar of one the equivalent definitions of monoidal (∞,n) category, and sketch how any stable (∞,1)-category should be presentable as a pointed (Z,1)-category.
Time permitting, we will then argue that this perspective suggests a syntax for homotopy dependent linear type theory, a conjectured type theory which should have models in all infinity topoi of parameterized stable infinity categories.
Dan Licata: 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. 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. In this talk, I will describe this framework, and show how it can be used to encode a variety of modal dependent type theories.
Giulio Lo Monaco: Set-theoretic remarks on a possible definition of elementary ∞-topos [slides]
In axiomatizing the significance of ∞-toposes in homotopy type theory, one realizes that dependent products and sums should be required to be recoverable within suitable classes of morphisms, namely some classes for which there exists a classifier. However, asking this of dependent products turns out to be a quite strong request. In fact, once we fix a Grothendieck universe, the possibility of finding classes of morphisms in an ∞-topos which both have a classifier and are closed under dependent products will be proven to be equivalent to the universe being 1-inaccessible, a condition which is strictly stronger than merely being inaccessible.
Andreas Lynge: Universal Algebra in HoTT [slides]
In this talk I will present our work on formalising universal algebra in HoTT. Universal algebra is a mathematical theory of algebraic structures. The isomorphism theorems in universal algebra are generalisations of the isomorphism theorems known from group theory and ring theory. In universal algebra, these theorems apply to all algebras, e.g. groups, rings, groups acting on sets, etc. Universal algebra has been developed in Coq by Spitters and van der Weegen, and in Agda by Gunther et al. To implement quotient types and function extensionality, these developments are using setoids, a type together with an equivalence relation. Setoids complicate the theory because maps between setoids are required to respect the equivalence relations, and existing theorems relying on strict equality do not apply to setoids. Higher inductive types can be used to define quotient types and the univalence axiom implies function extensionality. Motivated by this, we formalise universal algebra in the HoTT library using Coq’s type class mechanism in the style of the math-classes library. We give definitions of product algebra, subalgebra and quotient algebra. Product algebras are used to construct products in the category of algebras and homomorphisms, equalisers are subalgebras, and coequalisers are quotient algebras. Inspired by Coquand and Danielson, a central theorem in our development is that isomorphic algebras can be identified. Our development contains the three fundamental isomorphism theorems, which become identification theorems in HoTT. A longer description of the formalisation is available at https://github.com/andreaslyn/Work/blob/master/Math-Bachelor.pdf.
Hugo Moeneclaey: Toward a Cubical Type Theory with Univalence by Definition [slides]
We report on our progress in the construction of a variant of cubical type theory where univalence holds by definition, i.e. an inhabitant of A =type B is by definition an equivalence between A and B.
We take from [1] the definition of equivalences as relations satisfying an extra property. Following [2] we use an interval characterizing equality. So we need to define reduction rules e.g. for the transport along an equivalence of the form (lambda i.M) with i a dimension name and M a type depending on i. Those reductions are defined by induction on the construction of the type M, guided by ideas from parametricity. We pay a particular attention to the case where M is of the form A=type B with A and B depending on i.
[1] Towards a cubical type theory without an interval, T. Altenkirch and A. Kaposi (http://eprints.nottingham.ac.uk/44008/1/types.pdf)
[2] Cubical Type Theory: a constructive interpretation of the univalence axiom, C. Cohen, T. Coquand, S. Huber and A. Mörtberg (https://arxiv.org/abs/1611.02108)
Anders Mörtberg: A Unifying Cartesian Cubical Set Model [slides]
We present a new constructive model of univalent type theory based on cubical sets. The difference from earlier work on similar models is that it depends neither on “diagonal cofibrations” nor on connections or reversals. The key idea is to weaken the notion of fibration from the cartesian cubical model so that it is not necessary to assume that the diagonal on the interval is a cofibration. Our notion of fibration coincides with that of the existing cartesian and De Morgan cubical set models in the presence of the additional structures of the respective models. This notion of fibration also gives rise to a model structure, generalizing earlier work of Sattler to cubical sets without connections.
This is joint work with Evan Cavallo and Andrew Swan.
David Jaz Myers: Looking at Functions through the Modal Prism [slides]
A modality is a way to change what it means to identify two terms of a type. The n-truncation modality asks for an identification to only contain n homotopical dimensions of information, while the shape modality of Shulman’s Cohesive HoTT allows us to identify points by giving a continuous path between them. In this talk, we will see functions through the modal prism. There are many notions of function associated to a modality in use: modally truncated, modally connected, modally etale, modal covering. To these we will add the notions of a modal fibration and a modally constant family, and organize them all into a single diagram: the modal prism.
We will then see how these notions can be used to do algebraic topology in Real Cohesive HoTT. As an example, we will calculate the homotopy type of the topological circle { (x,y) ∈ R2 ❘ x2 + y2 = 1} without first expressing it as a higher inductive type.
Paige North: Towards a Higher Structure Identity Principle - a progress report [slides]
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, we discuss work in progress towards a Higher Structure Identity Principle in univalent foundations, for structures that naturally form a higher category (e.g., categories themselves).
This project is joint work with Benedikt Ahrens, Mike Shulman, and Dimitris Tsementzis.
Andrew Pitts: Presheaves, Constructive Sets and Univalence [slides]
Presheaf categories have been used to make models of univalent type theory, first in classical set theory (Voevodsky et al) and later in some form of constructive set theory (Coquand et al). Here I will concentrate on Intuitionistic Zermelo-Fraenkel set theory with Atoms (IZFA). Back in 1980 it was noticed by Mike Fourman, Dana Scott and others that to every presheaf category [Cop,Set] one can associate a Kripke-like forcing interpretation of IZFA. Within that model of set theory there is a category of “global” sets and functions equivalent to [Cop,Set] (and within that, a full subcategory equivalent to C). From this point of view, by relaxing from classical to intuitionistic logic, without loss of generality one can regard presheaves and their morphisms as just some particular sets and functions. So things that one might do concretely with presheaves (models of univalence!) can in principle be done in IZFA set theory and might look simpler there, because the set-theoretic interpretation of dependent types is straightforward. In this talk I will explore what is needed for a universe of sets in IZFA to model univalence, concentrating on the case when intensional equality is given by paths from an “interval” set.
Emily Riehl: The equivariant uniform Kan fibration model of cubical homotopy type theory
In joint work with Steve Awodey, Evan Cavallo, Thierry Coquand, and Christian Sattler, we introduce a constructive model for homotopy type theory on a category of cubical sets that defines a model category that is Quillen equivalent to spaces and supports “cellularly-inductive” constructions. This latter property is a feature of the cube category we use: the cartesian cube category, which is an Eilenberg-Zilber generalized Reedy category. Our model is a variation of ABCFHL obtained by demanding that the fibrations satisfy an additional equivariance condition on top of the uniform Kan condition. As a consequence, all quotients of cubes by groups of symmetries are contractible. Time permitting, we sketch the proof of the comparison Quillen equivalence, which makes heavy use of these contractible cube quotients.
Egbert Rijke: Agda formalization of homotopy pullbacks and pushouts using cubical diagrams [slides]
I would like to present a library of results on homotopy pushouts and pullbacks written in a subsystem of Agda. In this library of about 6000 lines of code, pullbacks and pushouts are specified via their universal properties, but there is no general assumption that universes are closed under pushouts, or that they even exist, and pushouts are also not assumed to satisfy strict computation rules on the point constructors. Using cubical diagrams, we first show that in a commuting cube, if the bottoms square is a pullback square then the top square is a pullback square if and only if it is fiberwise a pullback square. This result is then used to derive the dependent universal property of pushouts from the ordinary universal property of pushouts. With the dependent universal property of pushouts we use cubical diagrams again to show that pushouts are universal, i.e. that pullbacks of pushouts are pushouts again, and we phrase the descent property of pushouts using cubical diagrams, following the paper of Anel, Biederman, Finster, and Joyal. We also use our methods to give a straightforward characterization of the identity types of pushouts.
Robert Rose: Constructing the natural numbers in intensional type theories with S1 [slides]
Rijke and Shulman conjectured that the higher inductive type S1 might be viewed as an “axiom of infinity”: that well-founded types, such as the natural numbers, with their induction principles, might be obtained from the loop space of S1 in impredicative ITT with S1. The conjecture has a positive answer. The derived induction principle for the natural numbers applies to families of types in the cumulative hierarchy of univalent universes with propositional resizing. Of foundational interest, the proof also goes through in settings where suitable large elimination rules and a univalent universe of propositions, but not necessarily univalent universes, are available. However, in the presence of a univalent universe, an alternate proof is possible which has the virtue of being predicative. The automation of these results in Agda will be discussed.
Christian Sattler: Homotopy canonicity [slides]
Because of the axioms of univalence and function extensionality, homotopy type theory does not satisfy 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 proof of homotopy canonicity. This is joint work with Chris Kapulkin.
Filippo Sestini: Naturality for free (the category interpretation of directed type theory) [slides]
The idea that types are abstract, that is they cannot be inspected, underlies parametricity in particular the “free theorem” that all polymorphic functions are natural, and univalence (isomorphic types are equal). What is the relation between these two principles? We design a directed type theory which is inspired by a refinement of the groupoid model, replacing groupoids by categories. This Type Theory features polarities, directed version of the usual type formers (Pi and Sigma), a directed hom-type replacing symmetric equality and an operation “core” that constructs the groupoid of invertible maps, a directed form of path induction and directed univalence. From these principle we can derive both the usual univalence for groupoids and naturality for polymorphic functions. Our theory is truncated but we envisage that the syntax semantics can be extended to higher categories using complete Segal spaces.
The proposal is related to recent work by Paige North. We acknowledge useful discussions with her and with Dirk Pattinson.
Michael Shulman: All (∞,1)-toposes have strict univalent universes [slides]
We prove the conjecture that any Grothendieck (∞,1)-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to (∞,1)-toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.
Matthieu Sozeau: Equations for HoTT [slides]
The Equations plugin (https://mattam82.github.io/Coq-Equations) is a function definition package for Coq. The input language of Equations allows to define structural or well-founded functions by their defining equations, and naturally supports dependent pattern-matching. An elaboration produces axiom-free Coq terms from Equations definitions that can be checked by the vanilla Coq kernel. The support for dependent pattern-matching is compatible with HoTT in the sense that it can rely on path equality and does not require the UIP principle. Rather, it uses a form of definitional no-confusion principle to simplify equalities between constructors in inductive families, relying on the notion of “forced” arguments. This can be phrased as an encode-decode method for characterizing the path space in a specific instance of an inductive family. We additionally rely on the fact that this type equivalence is “strong” in a sense I will make precise. This provides an alternative solution to the interpretation of dependent pattern-matching using higher-dimensional unification introduced by Cockx & Devriese in Agda, which is also relatively easy to implement and compatible with Coq’s syntactic guardedness check.
Equations also provides for each function an inductive definition of its graph and an associated elimination principle, whose correctness and completeness are automatically proven: this provides an alternative charaterisation of the fiber of the function, which can be helpful for reasoning. Finally, besides providing a definitional compilation of dependent pattern-matching to type theory, a set of tactics dealing with dependent elimination and induction are provided, which can greatly help reasoning with inductive families in HoTT. In particular, these tactics also allow using the fact that some type is provably an HSet, so enjoy UIP, to simplify elimination problems and re-introduce a controlled, safe amount of the K rule in the interpretation of dependent pattern-matching.
Raffael Stenzel: Univalence and completeness of Segal objects [slides]
In this talk, we make precise an analogy between univalence and completeness that has been subject to informal discussions in the research community. More precisely, we give a definition of univalence and a definition of Rezk-completeness for Segal objects X in a large class of type theoretic model categories M. The former is a straightforward generalization of univalence in the type theoretic fibration category C of fibrant objects in M as treated in [3]. The latter is a generalization of Rezk’s original definition of completeness for Segal spaces. Both conditions share the heuristic purpose to contract a respective object of internal equivalences associated to X over the object X0 of points, turning that object of internal equivalences into a path object for X0. A priori, these objects of internal equivalences do not necessarily coincide, so the goal of this talk is to show the following theorem.
Let X be a “sufficiently fibrant” Segal object in M. Then X is univalent if and only if its Reedy fibrant replacement RX is complete.
As a corollary we obtain that a fibration in C is univalent if and only if the Reedy fibrant replacement of its nerve in M is Rezk-complete (this comparison in fact is independent of its infinity-categorical version presented in [2]). This implies for instance that univalent completion of a Kan fibration as introduced in [1] is a special case of Rezk completion of its associated Segal space.
[1] Van den Berg, Moerdijk - Univalent Completion
[2] Rasekh - Complete Segal objects
[3] Shulman - Univalence for inverse diagrams and homotopy canonicity
Jonathan Sterling: XTT: Cubical Exact Equality and Categorical Gluing [slides]
We contribute XTT, a cubical reconstruction of Observational Type Theory which extends intensional type theory with a dependent equality type that enjoys function extensionality and judgmental unicity of identity proofs. XTT employs a variant of the Cartesian cubical Kan operations satisfying regularity (i.e., transport in constant type families is judgmentally constant), allowing its equality type to model Martin-Lof’s identity type judgmentally. We prove canonicity for the initial model of XTT (i.e., any closed term of boolean type is equal to either true or false) using a novel cubical extension (independently proposed by Awodey) of the categorical gluing technique inspired by Coquand and Shulman, in which we glue the fundamental fibration of a category of augmented Cartesian cubical sets along a cubical nerve. We conjecture that our methods will extend to open terms, allowing us to establish normalization and decidability of the typing relation.
Chaitanya Leena Subramaniam: Contextual categories as monoids in a category of collections [slides]
Lawvere theories and (coloured) operads provide particularly nice representations for suitable algebraic theories with a given set of sorts, as monoids in certain categories of collections.
We extend this to dependently-sorted algebraic theories: For an inverse category I, we show how suitable “I-sorted contextual categories” may be viewed as monoids in a category of “I-collections”, and also as generalised Lawvere theories in the sense of Berger–Melliès–Weber. When I is a set, we recover the usual definition of I-sorted Lawvere theory.
Andrew Swan: On Church’s Thesis in Cubical Assemblies [slides]
The axiom of Church’s thesis states that all functions from the naturals to the naturals are computable. I will talk about two new results on Church’s thesis in cubical assemblies. The first is that Church’s thesis is false in the cubical assemblies model of cubical type theory itself. The second is that Church’s thesis holds in a reflective subuniverse (or more precisely lex modality) of cubical assemblies, and is therefore consistent with univalent type theory.
Karol Szumilo: Internal Languages of Higher Categories [slides]
Lambek and Scott proved that λ-calculus is the internal language of cartesian closed categories which they formalized as an equivalence between the category of λ-calculi and the category of cartesian closed categories. Similarly, they showed that the category of higher intuitionistic type theories is (nearly) equivalent to the category of elementary toposes. I will present joint work with Chris Kapulkin in which we investigate HoTT variants of such statements, i.e., that certain (∞,1)-categories of homotopy type theories (e.g., ones with identity types and Σ-types) are equivalent to certain (∞,1)-categories of (∞,1)-categories (e.g., ones with finite limits).
Taichi Uemura: A General Framework for the Semantics of Type Theory [slides]
We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin-Löf type theory, two-level type theory and cubical type theory. We establish basic results in the semantics of type theory: every type theory has a bi-initial model; every model of a type theory has its internal language; the category of theories over a type theory is bi-equivalent to a full sub-2-category of the 2-category of models of the type theory.
Benno van den Berg: Uniform Kan fibrations in simplicial sets [slides]
One of the open questions in homotopy type theory is whether it is possible to construct the Kan-Quillen model structure and a model of univalent type theory in the category of simplicial sets in a constructive metatheory (think: CZF with some universes). It is generally expected that the key must be in identifying the right uniformity conditions for the horn fillers. Together with Eric Faber, I am investigating one possibility (stronger than an earlier one by Gambino and Sattler). A crucial feature is that our definition is “local” (a map will have the structure of a uniform Kan fibration in our sense if every pullback to a map with a representable codomain does, and this structure is stable along pulling back along maps between representables). Right now, I am confident our definition gives one a model of type theory with Pi- and Id-types and a model structure on the fibrant objects. Clearly, more work remains to be done, so this will be a work in progress talk.
Matthew Z. Weaver: A Model of Type Theory with Directed Univalence in Bicubical Sets [slides]
Directed type theory is an analogue of homotopy type theory where types represent infinity-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 work, we investigate the extent to which the cubical techniques used to give computational models of homotopy type theory can be extended to a variant of the Riehl-Shulman directed type theory. Using Agda as the internal language of the presheaf topos of bicubical sets, we formalize the definitions of directed type theory, reformulate them to better correspond to the filling problems of cubical type theory, and implement them for various type constructors. We show that there is a universe of covariant discrete fibrations (covariant functors valued in types that themselves have trivial morphism structure), where functions are a retraction of morphisms in this universe. This retraction is “three quarters” of the desired directed univalence equivalence between functions and morphisms. We also describe some work in progress towards the final quarter, inspired by Sattler and Riehl’s proof of directed univalence in the bisimplicial model. Adapting their method to the bicubical setting is a significant extension, because simplices have a special property of being Reedy, which cubes lack. The approach we are currently investigating involves defining a Reedy category of prismatic sets, showing that cubical sets are equivalent to sheaves on prisms, and showing that the type theory’s fibrations can be interpreted in the model structure transfrered from prisms. This final quarter of the proof is not obviously non-constructive, though it will take further work to determine whether it has computational content.
Jonathan Weinberger: Type-theoretic modalities for synthetic (∞,1)-categories [slides]
It is a challenge to find a convenient type-theoretic formulation of (∞,1)-category theory. In a recent approach inspired by the complete Segal space model of (∞,1)-categories, Riehl and Shulman [RS17] devise a type theory compatible with Voevodsky’s univalence axiom yielding basic results of (∞,1)-category theory. We present a variation of Riehl and Shulman’s theory, extended by certain modalities in order to derive new results in this framework. Some of these modalities first appeared in connection with manifold-like cohesion, cf. [Shu18]. As an example, we give an actual embedding of categories yA: A → (Aop → Space) illustrating two new features: the opposite modality (-)op, and a categorical universe of spaces and maps, Space. In order to be able to make this construction we introduce new operations on the level of topes allowing for defining twisted arrow types. The intended semantics is – as in Riehl–Shulman’s work – in a model structure presenting simplicial spaces but embedded in cubical spaces. This allows for an internal definition of the universe Space due to techniques developed by Licata–Orton–Pitts–Spitters [LOPS18]. We also give countermodels in truncated simplicial sets showing that modal discreteness, i.e. being modal with respect to the discrete modality, does not in general coincide with categorical discreteness, by which we mean the internal notion of discreteness used in Riehl–Shulman’s type theory (i.e. invertibility of all directed arrows in a type).
This is joint work with Ulrik Buchholtz.
David White: Monoidal Model Categories and Cubical Homotopy Theory [slides]
In this talk, I will present a proof that the arrow category of a monoidal model category, equipped with the pushout product monoidal structure and the projective model structure, is a monoidal model category. This answers a question posed by Mark Hovey, and has the important consequence that it allows for the consideration of a monoidal product in cubical homotopy theory. If there is time, I will discuss connections to homotopy type theory, to the theory of Smith ideals of ring spectra, and to a recent operadic generalization of Smith ideals. This talk is joint work with Donald Yau.
Colin Zwanziger: Natural Model Semantics of Comonadic Modal Type Theory [slides]
While comonadic modal type theory has been extended to the dependently-typed setting (Nanevski et al., 2008; Shulman, 2018), the semantics of such comonadic modal dependent type theories remains underexplored. This gap in the literature takes on particular urgency in light of the active use of such type theories in the homotopy type theory community (Shulman, op. cit.; Licata et al., 2018). Here, we give a semantics for Shulman (op. cit.)’s comonadic dependent type operator in the framework of natural models and their morphisms. This is apparently the first formal suggestion for a model of a fully dependent comonadic type theory. Natural models were developed (Awodey, 2018) as an equivalent, category-theoretic formulation of categories with families (CwFs, Dybjer, 1995), the popular categorical semantics for dependent type theory. To interpret the comonadic operator, we introduce what we call a (weak) Cartesian comonad on a natural model. This makes use of the promising idea of a weak morphism of natural models (Newstead, 2018) or CwFs (Clouston et al., 2018). While “Cartesian comonad of natural models” is an appealingly simple description, the actual interpretation with respect to such a comonad involves some exercise. The two-zone contexts of the type theory are interpreted not as objects of the underlying category of contexts, but as morphisms with codomain a coalgebra. The requirement that the comonad be a morphism of natural models is seen to impose the correct relationship between the comonadic operator and the usual induced relative comonad. We also mention a formulation in terms of CwFs.
Reception and Dinner
Reception
There will be a reception Monday evening from 5:30–6:30 at the Schenley Park Visitor’s Center. The location is on the conference google map and shown below:
Dinner
There will be a conference dinner Thursday evening at 6:00 at the Hotel Indigo. The location is on the conference google map and shown below:
Excursions
On Wednesday afternoon, local organizers will lead excursions to Mount Washington and a cruise of Pittsburgh’s “three rivers”. There are also several suggestions for self-guided excursions. All the excursion destinations are marked on the conference google map.
Guided Excursions
The guided excursions will depart from the coffee area outside Giant Eagle Auditorium at 2:15 pm on Wednesday the 14th. Local organizers will conduct the group to (and from) Station Square near downtown, via the frequent public buses. At Station Sq., the groups will diverge.
Mount Washington
Mount Washington is a pleasant hilltop neighborhood that offers excellent views of Pittsburgh’s historic city center. The group will ascend and descend the hill via the inclined railways, completing a loop including 1.7 miles of walking. The cost of the inclined railways is $5.
Gateway Clipper Cruise
Cruise the rivers of Pittsburgh, with excellent views of Pittsburgh’s historic city center. The cruise is conducted by Gateway Clipper and includes some narration about the city. The cost of a ticket is $22, but can be reduced to $11 using a coupon in the coupon booklet. The cruise departs Station Square at 3:30 pm and lasts an hour.
Self-guided Excursions
Phipps Conservatory and Botanical Gardens
An extensive botanical garden walking distance from the CMU campus (http://www.phipps.conservatory.org), in Schenley Park. A coupon in the coupon booklet gives 10% off.
Carnegie Museums of Art and Natural History
Pittsburgh’s primary museum complex (https://carnegiemuseums.org/), walking distance from CMU. The natural history museum is particularly noted for its dinosaur and gemstone collections.
Schenley and Frick Parks Hiking Trails
Schenley and Frick Parks are large and rustic parks within Pittsburgh, offering hiking trails. Schenley Park is right out the door of Baker Hall, whereas the rustic trails at Frick Park are more extensive.
Carrie Blast Furnaces National Historic Landmark
Tours of an old industrial steel furnace conducted by former steel workers (https://riversofsteel.com/attractions/carrie-furnaces/). Note that the afternoon tour on Wednesday departs at 1 pm, however.
The Andy Warhol Museum
Extensive museum devoted to the famous Pittsburgh artist (https://www.warhol.org/).
The Frick Pittsburgh
Gilded Age mansion of steel magnate Henry Frick (https://www.thefrickpittsburgh.org/). Adjacent museum is noted for its car and carriage collection.