# Stockholm–Göteborg type theory seminar

**Time: **
Thu 2020-02-27 11.00 - 17.00

**Location: **
Chalmers University, Gothenburg

Thursday, 27 Feb, c.11:00–17:00

Göteborg University

Precise time and location TBA

This will be the 4th meeting of the irregular joint Stockholm–Göteborg type theory seminar! This instance will take place at Chalmers University, with speakers from Göteborg and Stockholm. Details of programme below; the meeting will start late morning (11:00 at earliest) and continue through the afternoon (until 17:00 at latest), with an early dinner afterwards.

For travellers from Stockholm: the 7:30 train from Stockholm C (arriving 10:35 Göteborg C) and the return trains leaving Göteborg C at 18:24 or 20:24 should be suitable.

———————————————

11:30 Nils Anders Danielsson: Logical properties of a modality for erasure

12:15 Lunch

13:30 Oscar Berndal: Presenting first order logic as a type theory

14:15 Max Zeuner: A cubical approach to the Structure Identity Principle

14:30 Fabian Ruch: Lex modality from a well-pointed lex operation

14:45 Ayberk Tosun: Formal topology in Univalent Foundations

15:00 Coffee

15:30 Peter Lumsdaine: Equivalences of models of type theories

This is an informal workshop and times are preliminary.

All talks are in room 8103 in the EDIT building, Rännvägen 6B. (The room is rather hard to find; directions are at http://maps.chalmers.se/#edfe7e18-1688-487d-8b67-3d3073d7134a.)

———————————————

Nils Anders Danielsson: Logical properties of a modality for erasure

Abstract:

In dependently typed languages one can have redundant data that is used for typing but not really needed for computing things. That can be a problem when it comes to performance, and there are several ways to address this problem. One of these approaches, due to McBride and Atkey, is type-based and involves annotating things that should be erased.

This approach allows you to define a type constructor Erased. Erased is similar to an identity function for types, but values of type Erased A should be erased by the compiler. The typing rules are designed to ensure that one never gets into a situation in which a program has to make a decision based on an erased piece of data, and this arguably makes the theory of Erased more interesting than that of the identity function.

I plan to present some theory of Erased, which turns out to be a left exact modality in the sense of Rijke, Shulman and Spitters. As a running example I have an implementation of natural numbers that computes roughly like unary natural numbers at compile-time (for some operations), but like binary natural numbers at run-time.

————

Oscar Berndal: Presenting First Order Logic as a Type Theory

Abstract:

The aim of this talk is to understand the functorial semantics for first order logic as semantics for some type theory. We rely on recent work by Uemura to present a type theory and retrieve a corresponding semantics.

An obstacle is the mismatch between what one takes as a morphism in the initial model: In first order logic one takes the functional relations whereas in type theory one essentially takes the terms. In order to bridge this gap we introduce terms for definite descriptions to the type theory.

This way we can understand some aspects of the functorial semantics as semantics for the type theory: Their initial models are equivalent and Heyting functors out of the initial model correspond to certain models of the type theory. Hopefully we will also find time to discuss how the natural transformations of Heyting functors still elude this viewpoint.

————

Max Zeuner: A cubical approach to the Structure Identity Principle

Abstract: The structure identity principle (SIP) is an informal principle, which asserts that reasoning about mathematical structures is invariant under isomorphisms of such structures. This can be made precise in HoTT/UF and formalized versions of the SIP have been proved for large classes of mathematical structures. We will discuss a version of the SIP that can be found in the lecture notes of Martín Escardó and our work can be seen as a reformulation of it in cubical type theory. By reformulating the SIP cubically some of the key proofs become more direct than in HoTT/UF, and furthermore, the cubical SIP lets us transport programs and proofs between isomorphic structures without sacrificing the computational content of the transported programs and proofs. We will then discuss a few examples to demonstrate how the cubical SIP is applied to actual instances of structures in mathematics and computer science.

(Joint work with Anders Mörtberg.)

————

Fabian Ruch

Title: Lex modality from a well-pointed lex operation

Abstract: Locales and nuclei can be seen as preorder versions of higher toposes and lex modalities. Here we take higher toposes to mean models of univalent type theory and the interest in lex modalities lies in constructing new models from old ones. Nuclei are generated by

(1) inflationary (x ⩽ j(x))

(2) meet-preserving (j(x ∧ y) = j(x) ∧ j(y))

maps on frames called prenuclei and their fixpoints form a new frame. Analogously,

(1') well-pointed

(2') lex

operations on models of univalent type theory generate lex modalities and their modal types form a new model.

————

Peter LeFanu Lumsdaine: Equivalences of models of type theories

Abstract: The *inverse diagram models* of Lumsdaine-Kapulkin arXiv:1808.01816, arXiv:1610.00037 give a notion of equivalence of models of type theories (somewhat formally analogous equivalence of categories), and techniques for constructing such equivalences. I will present these together with a couple applications, including that models are “robust under perturbation of the interpretation of constructors”, and conservativity/equivalence results between certain type theories.