Programme

Thursday 3 December: Room 35, Hus 5, Kräftriket

13:30–14:30 Thierry Coquand — Cubical Type Theory
    coffee break
14:45–15:25 Marek Zawadowski — Fibrations of polynomial and analytic functors and monads
15:25–16:05 Staffan Angere — Modal logics for weak categorical constructions
16:05–16:45 Håkon Robbestad Gylterud — A coalgebraic view on dependent types and terms
    coffee break
17:00–18:00 Henrik Forssell — Constructive completeness and non-discrete languages
    19:00: table booked at Alfeus

Friday 4 December: Room 306, Hus 6, Kräftriket

    from 9:00: coffee etc.
9:30–10:30 Michael Makkai — Sketch-theoretic reformulations of Michael Batanin’s concept of weak higher category and its variants
    coffee break
10:40–11:20 Zhen Lin Low — Another viewpoint on cartesian theories
11:20–12:00 Dimitris Tsementzis — n-logic: model theory in the framework of UF
    lunch break — table booked at Kräftan
13:30–14:30 Nicola Gambino — On the simplicial and cubical models of type theory
    coffee break
14:45–15:25 Rasmus Mogelberg — Denotational semantics in guarded dependent type theory
15:25–16:05 Stephan Spahn — A relationally-parametric model of Martin-Löf Type Theory with induction-recursion
16:05–16:45 Samuele Maschio — A strictly predicative version of Hyland’s effective topos
    coffee break
17:00–18:00 Peter Dybjer — Undecidability of equality in the free locally cartesian closed category

Invited talk abstracts

Thierry Coquand: Cubical Type Theory

(Joint work with Cyril Cohen, Simon Huber and Anders Mörtberg.)

We present the syntax and semantics of an extension of type theory. We add two new operatons on contexts: addition of a new dimension/name/symbol and a restriction operation. Using these operations, we can define a notion of connectedness which generalizes the notion of being path-connected, and then a Kan composition operation which expresses that being connected is preserved along paths, and a new operation on types which expresses that this notion of connectedness is preserved by equivalences. The axiom of univalence is provable in this type theory (in the form suggested by Martin Escardo). Using ideas from Andrew Swan, we also can represent Martin-Löf’s identity type which is equivalent to, but not convertible to the path type. We also can represent some form of higher inductive types, such as propositional truncation, and in this way provide a new explanation of the axiom of definite description.

Peter Dybjer: Undecidability of equality in the free locally cartesian closed category

(Joint work with Simon Castellan and Pierre Clairambault.)

We show that a version of Martin-Löf type theory with extensional identity, a unit type N_1, Σ, Π, and a base type is a free category with families (supporting these type formers) both in a 1- and a 2-categorical sense. It follows that the underlying category of contexts is a free locally cartesian closed category in a 2-categorical sense because of a previously proved biequivalence. We then show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic.

Henrik Forssell: Constructive completeness and non-discrete languages

We give an analysis in terms of categorical logic and pre-sheaf and sheaf semantics of some long-established constructive completeness results, and add some new results in this area which flow from the analysis. The purpose is in no small part conceptual and organizational: from a few basic ingredients arises a more unified picture connecting constructive completeness with respect to Tarski semantics, to the extent that it is available, with various completeness theorems in terms of presheaf and sheaf semantics (and thus with Kripke and Beth semantics). From this picture are obtained both (``reverse mathematical’’) equivalence results and new constructive completeness theorems; in particular, the basic set-up is flexible enough to obtain strong constructive completeness results for languages over non-discrete signatures.

This is joint work with Christian Espindola and Peter LeFanu Lumsdaine.

Nicola Gambino: On the simplicial and cubical models of type theory

As shown by Voevodsky, Martin-Löf type theory extended with the univalence axiom admits a model in the category of simplicial sets, which is defined within classical set theory. In an effort to prove Voevodsky’s canonicity conjecture, Coquand and his collaborators have developed constructive counterparts of the simplicial model. This work involves two main aspects: moving from simplicial sets to cubical sets and working with algebraic variants of the notion of a Kan fibration. The aim of the seminar is to give a survey of the simplicial and cubical models and describe the motivations for some recent work done by Christian Sattler and Andrew Swan in Leeds.

Michael Makkai: Sketch-theoretic reformulations of Michael Batanin’s concept of weak higher category and its variants

Extended abstract and full slides from previous talk on the subject (Ottawa, October 2015).

Contributed talk abstracts

The talk presents a class of first-order modal logics, called transformational logics, which are designed for working with relations that hold up to a certain type of model homomorphism. A sound and complete inference system is given for the basic logic HOS, which deals with arbitrary Homomorphisms Onto Submodels. As a second step, I give an interpretation of infinity-precategories as first-order structures, with model homomorphisms as functors. Classes of homomorphisms between these correspond to various forms of equivalence such as isomorphism, category equivalence, and homotopy equivalence. In particular, we will see that category equivalence literally comes out as “isomorphism up to isomorphism”. This allows the use of transformational logics to define both weak higher categories and structures in 1-categories that are defined only up to equivalence. As examples, I will show how to give simple definitions of bi- and tricategories, and how a rather straightforward addition of an epsilon operator can be used to introduce terms for “the” Cartesian product of two objects in a 1-category, even if such products are only defined up to isomorphism.

Håkon Robbestad Gylterud: A coalgebraic view on dependent types and terms

Coalgebras are versatile tools with uses in logic, theoretical computer science and topology — among others. One way to describe a coalgebraic structure is that the coalgebraic operation decomposes the objects of the structure to reveal some of their structure and relationships.

In this talk we will investigate a coalgebraic approach to dependent types and terms, in which the coalgebraic operation reveal the dependencies between types and terms.

Zhen Lin Low: Another viewpoint on cartesian theories

As is well known, cartesian theories have essentially the same expressive power as finite limit sketches, but some details are lost in the translation: for instance, a cartesian theory has an underlying algebraic theory, but this disappears after passing to the syntactic category. The gap can be bridged by introducing the notion of cartesian hyperdoctrine. Such a structure gives rise to a category of fibrant objects, and in the case of the cartesian hyperdoctrine generated by a cartesian theory T, its homotopy category is the syntactic category of T.

Samuele Maschio: A strictly predicative version of Hyland’s effective topos

(Joint work with Maria Emilia Maietti; pdf version with references.)

The tripos-to-topos construction by Hyland-Johnstone-Pitts provides a powerful machinery in categorical logic to build examples of elementary toposes suitable for modelling various set theories. The most famous and seminal example is Hyland’s effective topos which hosts a model of IZF.

A predicative generalization of Hyland’s effective topos had been studied by Moerdijk and van den Berg by referring to CZF as the set theory to be modelled.

Here we generalize the notion of tripos-to-topos to a strictly predicative version (à la Feferman) to build a categorical universe for the (extensional level of the) Minimalist Foundation (for short MF) conceived by Maietti-Sambin in 2005 and completed in 2009.

We base our construction on a categorical presentation of the model for the intensional level of MF that we call predicative effective tripos. The adjective predicative refers to the fact that the tripos is formalized in Feferman’s theory of inductive definitions ID1 and the adjective effective to the fact that the model validates the extended Church thesis. Then we perform the elementary quotient completion on such a tripos and the resulting category can be considered as a strictly predicative version of Hyland’s effective topos.

Rasmus Mogelberg: Denotational semantics in guarded dependent type theory

Joint work with Marco Paviotti and Lars Birkedal.

Guarded dependent type theory (gDTT) is a type theory for modelling recursion. It can be modelled using an indexed family of presheaf categories. In this talk I study how to use gDTT as a metalanguage for denotational semantics. More precisely I show how to construct a model of PCF (simply typed lambda calculus with natural numbers and a call-by-value operational semantics) and prove an intensional computational adequacy result entirely in gDTT. Moreover, I show how to capture the usual extensional contextual equivalence of PCF programs in the model using a logical relation.

Stephan Spahn: A relationally-parametric model of Martin-Löf Type Theory with induction-recursion

(Joint work with with Neil Ghani and Fredrik Nordvall-Forsberg.)

We will extend the relationally-parametric model of dependent type theory of [Atkey, Johann and Ghani, 2013] to a model of Martin-Löf type theory extended by induction-recursion as presented in [Dybjer and Setzer, 2003]. The involved reflexive graph model of IR-codes and -types is itself defined by indexed induction-recursion.

Dimitris Tsementzis: n-logic: model theory in the framework of UF

A fundamental idea in UF is that “n-level” structures are best understood as structures defined on homotopy n-types. For example, (univalent) categories are best understood as structures on groupoids (homotopy 1-types). I define a proof-irrelevant logic, called n-logic, that makes good on this idea (for -1 ≤ n < ∞). I will begin by describing the syntax of n-logic as an extension of Makkai’s FOLDS analogous to the extension of first-order logic to first-order logic with equality. The basic idea is to take a FOLDS signature and then “globularly complete” all of its sorts to obtain an expanded signature. I will then describe the intended semantics for this syntax in UF, based on the above-described fundamental idea: given a signature L of n-logic, an L-structure will be a structure defined on a homotopy n-type (as the latter is defined within UF). Then I will describe a proof system that is sound for this semantics and sketch a proof of completeness for the case n = 1. Finally, as an application, I will prove that univalent categories are axiomatizable in 1-logic (i.e. are “1-elementary”).

Marek Zawadowski: Fibrations of polynomial and analytic functors and monads

(Joint work with Stanisław Szawiel.)

I will describe a framework that allows to define (various kinds of) polynomial and analytic (endo)functors in a uniform way. They arise as images of representations of Kleisli and Eilenberg–Moore 0-cells for a lax monoidal monad. Such monad is naturally derived from an action of a monoidal 0-cell on an exponentiable object in a 2-category C with some additional properties. If the monad in question preserves reflexive coequalizers, both Kleisli and Eilenberg–Moore 0-cells are equipped with monoidal structure that makes them Kleisli and Eilenberg–Moore 0-cells in the 2-category of monoidal objects in C. The tensor on the Eilenberg-Moore 0-cell is given Linton formula that dates back to 1969. In that case 0-cells of monoids (various operads and multicategories) are represented as polynomial and analytic monads. This can be further lifted to the Kleisli and Eilenberg–Moore 0-cells in the 2-category of actions of monoidal objects.

After describing the above general picture I will focus on two examples of polynomial and analytic functors. One due to Joyal defined on slices of the category Set and the other due to Fiore–Gambino–Hyland–Winskel defined on presheaf categories.