StockholmGoteborgMeeting200227
Stockholm–Göteborg meeting on Thursday, 27 February 2020 in Göteborg
Program
| Time | Speaker | Title |
|---|---|---|
| 11:30–12:15 | Nils Anders Danielsson | Logical properties of a modality for erasure |
| lunch | ||
| 13:30–14:15 | Oscar Berndal | Presenting First Order Logic as a Type Theory |
| 14:15–14:30 | Max Zeuner | A Cubical Approach to the Structure Identity Principle |
| 14:30–14:45 | Fabian Ruch | Lex modality from a well-pointed lex operation |
| 14:45–15:00 | Ayberk Tosun | Formal Topology in Univalent Foundations |
| fika | ||
| 15:30–16:15 | Peter Lumsdaine | Equivalences of models of type theories |
Abstracts
Nils Anders Danielsson — Logical properties of a modality for erasure
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
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
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 — Lex modality from a well-pointed lex operation
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
- inflationary (
x ⩽ j(x)) - meet-preserving (
j(x ∧ y) = j(x) ∧ j(y))
maps on frames called prenuclei and their fixpoints form a new frame. Analogously,
- well-pointed
- lex
operations on models of univalent type theory generate lex modalities and their modal types form a new model.
Ayberk Tosun — Formal Topology in Univalent Foundations
Developing topology in type theory involves understanding topology predicatively. For non-univalent type theories, this problem has been solved using structures known as formal topologies, formulated first by Martin-Löf and Sambin. In my talk, I will explain why formal topologies fail to work in univalent foundations as they are and how this problem can be remedied using HITs.
Peter Lumsdaine — Equivalences of models of type theories
The inverse diagram models of Lumsdaine–Kapulkin 2018, 2016 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.