Programme
Thorsten Altenkirch: homotopy type theory as a foundation for mathematics?
In my well-known neutral style I am going to discuss the advantages of Homotopy Type Theory as a foundations of Mathematics compared to last century approaches like first order logic and set theory.
Steve Awodey: a cubical fibrant replacement monad
I will consider an algebraic weak factorization system on cubical sets, using a variant of Garner’s small object argument.
Andrej Bauer: the Andromeda proof assistant
The Andromeda proof assistant is an LCF style proof assistant for type theory with equality reflection. The base theory supports only dependent products and equality types. Andromeda has no built-in notion of normalization or equality checking (the underlying type theory has undecidable equality checking). Instead, it provides a meta-language (AML) in which the user can implement various algorithms and extensions of type theory. AML guarantees that it will never compute an underivable judgement.
In this talk I will show how the user can implement in AML an equality checking algorithm for a normalizing fragment of type theory, how we can add new judgmental equality to the system and thereby implement new constructs, such as W-types and universes, and how we can implement implicit arguments and unification.
Benno van den Berg: a homotopy-theoretic model of function extensionality in the effective topos
Jaap van Oosten has presented a notion of homotopy in the effective topos based on a “path object” functor P : Eff → Eff, making P X an internal groupoid over X. From this he derives basic notions of abstract homotopy. This construction results in a path object category structure on Eff, and, consequently, a model of type theory. We choose to study homotopy in the subcategory of the effective topos consisting of fibrant objects, where the notion of fibrancy is induced by the interval object ∇2. We present a model category structure on the subcategory of Eff where cofibrations are monomorphism and weak equivalences are strong homotopy equivalences. This model category structure induces a model of type theory, in which the identity type for a type X is represented by Xᴵ. It follows that the resulting model supports functional extensionality.
(Joint work with Daniil Frumin.)
Paolo Capriotti: presheaf models of two-level type theory
Two-level type theory is a variation of HoTT (inspired by Voevodsky's HTS) where a “strict equality” type, satisfying UIP, is present alongside the usual higher dimensional identity type. In order for the two equalities to coexist, one has to distinguish a special class of types, called “fibrant”, for which the latter equality is defined. I will show how one can build a model of two-level type theory in presheaves over a model of HoTT, which will imply a conservativity property of two-level type theory over its fibrant fragment.
Thierry Coquand: a constructive model of homotopy types
I will present the cubical set model of type theory with univalence which is carried out in a constructive meta theory, explaining why we added diagonal operations in the model and how to represent some simple higher inductive types (without any coherence issues). I will then explain a recent canonicity result (Simon Huber) for the associated cubical type theory. I will also present some metatheoretical application of the formal representation of this model in NuPrl (Mack Bickford).
Nicolai Kraus: higher categorical structures and homotopy coherent diagrams
Categorical constructions internally in homotopy type theory are intricate. Without a notion of strict equality, the usual categorical laws can only be stated “up to homotopy” and should not be viewed as laws, but as structure of higher categories. Especially intriguing is our inability to talk about type-valued diagrams over a given category. In this talk, I want to give an overview over attempts to develop a theory of (∞,1)-categories via semi-Segal types. Further, for the case of inverse categories, I want to show how we can cleanly define homotopy coherent diagrams (weak functors that come with all higher coherences) and prove that they are equivalent to Reedy fibrant ones (strict functors that are defined levelwise). The talk is based on joint work with Thorsten Altenkirch and Paolo Capriotti, and with Christian Sattler.
Robert Harper: computational higher type theory
Since the inception of higher-dimensional type theory, the question of its constructive significance has been central. Familiar type theories, such as the Calculus of Constructions, admit a computational interpretation by virtue of its proof-theoretic properties. But consideration of such intriguing extensions as Voevodsky’s univalence axiom disrupts the properties on which such an interpretation depends. Consequently there has been considerable effort on establishing the constructive meaning of such extensions. A crucial advance is the development of formal cubical type theories (by Licata and Brunerie and by Coquand and his co-workers) that provide a directly judgmental account of paths within and among types. Whereas these are axiomatic theories defined by rules, we instead describe here an explicitly computational cubical type theory that directly explains the computational meaning of higher type theory, including the central notion of Kan composition. Our approach follows that of Martin-Löf’s “meaning explanations” of type theory, and may be seen as extending the semantics of the NuPRL type theory to higher dimensions. Alternatively, one may view the proposed interpretation as a meta-mathematical device for analyzing formal type theories using the new concept of cubical realizability. The main result is computational canonicity, stating that a closed zero-cell of boolean type evaluates to either true or false for a higher-dimensional dependent type theory with two higher inductive types and an instance of the univalence axiom.
(Joint work with Carlo Angiuli and Todd Wilson.)
Eric Palmgren: categories with families, FOLDS and logic enriched type theory
Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Löf type theory. Makkai’s first-order logic with dependent sorts (FOLDS) is an example of a so-called logic enriched type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and Aczel’s and Belo’s dependently typed (intuitionistic) first-order logic (DFOL) fit in this semantical framework. A soundness and completeness theorem is proved for such a logic. The semantics is functorial in the sense of Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra for a DFOL theory. Agreement with standard first-order semantics is established. Some applications of DFOL to constructive mathematics and categorical foundations are given. A key feature is a local propositions-as-types principle.
Egbert Rijke: principal equivalence relations
To define the finite dimensional complex projective spaces, we use a notion of orientation on the circle, defined as a type family on the type of all types merely equal to the circle. This allows us to extend the tautological bundle on ℂPⁿ to the tautological bundle on ℂPⁿ⁺¹, via its universal property and the univalence axiom.
The idea of orientations on the circle can be generalized to reflexive type-valued relations, viewing the circle as a reflexive relation on the unit type. The result is a notion of ∞-equivalence relation, which we call ‘principal equivalence relation’. Given a principal equivalence relation R on X, we define the quotient X/R as the (large) type of all oriented type families on X in the image of R. On an actual Prop-valued equivalence relation on a set X, the type of orientations is contractible, so this construction is directly generalizing Voevodsky’s impredicative construction of set-quotients.
The first thing we show about these quotients is that X/R classifies ‘oriented R-spans’, in a sense we will make precise. Secondly, we generalize the construction of the complex projective spaces to obtain a sequence of small types, defined as certain homotopy pushouts, of which the colimit is X/R. So we see that the construction of the projective spaces fits in this very general scheme of the ‘quotient approximation construction’, and moreover we use this approximation to argue that the quotient is equivalent to a small type. Since the quotient map X → X/R is surjective, this gives a map from the type of all principal equivalence relations, to the type of all surjective maps out of X into a small type. Now we proceed to show that this map is an equivalence. In other words, this proves that the quotienting operation is effective, and that the idea of orientability correctly captures a notion of ∞-equivalence relation.
Christian Sattler: a modular glueing construction
Cohen/Coquand/Huber/Mörtberg introduced the so-called glueing construction in the context of cubical type theory in order to make the universe into a type, though it was later realized to also relate to univalence. The combinatorial details of the construction are quite intricate due to the need to satisfy a number of constraints, some only arising because types are modelled as fibration structures in cubical sets with chosen lifts part of the data. We discuss a modular version of the glueing construction that decomposes the problem into a number of smaller constructions, separately addressing the constraints to be satisfied. Our construction works in the generic context of a functorial cylinder.
A talk based on the same material has been presented at the recent Fields workshop “Homotopy Type Theory and Univalent Foundations of Mathematics”.
Matthieu Sozeau: forcing translations in type theory
Forcing is a well-known technique introduced by Cohen to prove meta-theoretical results in Set Theory. Over time, the technique has been adapted, reformulated and used as an essential tool in metatheoretical studies, e.g. as Kripke models in logic and programming language theory. On the side of proof-theory and type theory, forcing can also be seen as a kind of translation from a theory to itself, “extending” its logical power and adding (limited) effects. On the side of category theory, there is the folklore idea that forcing is a presheaf construction. In this talk, we will show that while it certainly holds for what we see as a call-by-value version of forcing, it is not necessarily the case for our call-by-name flavor of forcing, the two versions being instances of a general call-by-push-value inspired decomposition of dependent type theory.
Our call-by-name translation of intensional type theory naturally respects definitional equalities, when combined with the Yoneda embedding and can be used to prove meta-theoretical results directly in vanila type theory. We will present examples of independence results obtained this way, including the independence of the Univalence Axiom.
(Joint work with G. Jaber, G. Lewertowsky, P.-M. Pédrot, and N. Tabareau.)
Andrew Swan: some constructions of split comprehension categories with application to realizability
I will show some general ways to produce new split comprehension categories (split CC's) from old using a few simple ideas and some well known results from categorical logic. The main motivating example is the Bezem-Coquand-Huber CwF of cubical sets, which is defined directly using Hofmann's interpretation of type theory in presheaf categories, instead of using any general coherence theorem. I will show this is an instance of a general construction, which combines a split CC with an algebraic weak factorisation system (awfs) to produce a new split CC. A second, related construction shows how to combine a split CC with an internal category in the base to produce a new split CC. This gives us a general version of Hofmann's interpretation of type theory in presheaves. Replacing the split CC of families of sets with the split CC of uniform families of assemblies (or modest sets, or realizability toposes) allows us to define a notion of presheaf assembly. This includes a split CC based on Stekelenburg's simplicial assemblies and also split CCs based on various notions of cubical assembly. Finally, by defining an awfs in cubical assemblies, we obtain a split CC where the objects of the total category (ie. the dependent types) consist of a family of cubical assemblies together with a computable Kan filling operator.
Dimitris Tsementzis: homotopy model theory
A model theory in the framework of Univalent Foundations requires a logic that allows us to define structures on homotopy (n-)types, similar to how first-order logic can define structures on sets. We define such an “n-level” logic for finite n. The syntax is based on a generalization of Makkai’s FOLDS, obtained by an operation that allows us to add equality sorts to FOLDS-signatures. We then give both a set-theoretic and a homotopy type-theoretic semantics for this logic and prove soundness for both with respect to an appropriate deductive system. As an application, we prove that univalent categories are axiomatizable in 1-logic.