TYPES in Munich

Supported by the Junior Researcher Fund, LMUexcellent

11-12 March 2020, Ludwig-Maximilians-Universität München

Venue Programme Abstracts TIM19 ✉ Chuangjie Xu

Venue

Due to insecurities concerning COVID-19, we turn the workshop into an online meeting. Here is the link to the online meeting room.

Room B349
Mathematisches Institut, LMU München
Theresienstr. 39
D-80333 Munich

Programme

Wednesday 11.03.2020

12:55 Opening
13:00 - 13:45 Max Zeuner: A Cubical Approach to the Structure Identity Principle
13:45 - 14:30 Nils Köpp: Program Analysis and Transformation via Monadic Translations
14:30 - 14:45 Break
14:45 - 15:30 Nicolai Kraus: An Induction Principle for Cycles
15:30 - 16:15 Felix Cherubini: Cohomology of Sheaves in Homotopy Type Theory
16:15 - 16:30 Break
16:30 - 17:30 Anders Mörtberg: A Tour of the Cubical Agda Library
17:30 - 18:00 Fredrik Nordvall Forsberg: "Dimensionally Correct by Construction" Programming

Abstracts

Felix Cherubini: Cohomology of Sheaves in Homotopy Type Theory
The general cohomology of parametrized spectra developed by Shulman and van Doorn contains as a special case the sheaf cohomology of algebraic topology and algebraic geometry. We give a couple of theorems about these cohomologies that are typically of interest in geometry.
Nils Köpp: Program Analysis and Transformation via Monadic Translations
We introduce a parametrized monadic translation of Gödel's System T (and possible extensions), and prove a corresponding fundamental theorem of logical relation. By instantiating the monad and the base case of the logical relation, we reveal various properties and structures of programs in T such as majorizability and (uniform) continuity.
Nicolai Kraus: An Induction Principle for Cycles
joint work with Jakob von Raumer

Consider paths in a given graph. If we want to prove a certain property for all paths, the obvious approach is to try induction on [the length of] paths. If we want to prove a certain property for all *closed* paths a.k.a. cycles (first vertex = last vertex), this does not work since closed paths are not inductively generated: if we remove an edge from a closed path, it is not closed any more.

We have studied this situation because certain coherence conditions in HoTT can be formulated in terms of cycles. The problem discussed above then makes it difficult to verify these conditions in the case of natural applications.

We build on the observation that, at least in all those cases we are interested in, the graph is given by the symmetric closure of a locally confluent and Noetherian (co-well-founded) proof-relevant relation. Under these assumptions, we construct a new Noetherian relation on cycles which allows co-well-founded induction. As a consequence, whenever we have to prove a property for all cycles, it suffices to prove the property for the empty cycle and for those given by local confluence.

An application in HoTT is the statement that the fundamental groups of the free higher group over a set are trivial.
Anders Mörtberg: A Tour of the Cubical Agda Library
We have found that many results that were difficult in HoTT is a lot easier to formalize cubically (e.g. the 3x3 lemma for pushouts) and I would love to get some ideas for other things to try.
Fredrik Nordvall Forsberg: "Dimensionally Correct by Construction" Programming
Chuangjie Xu: Statistical Approaches to Theories
I would like to discuss a seemingly possible application of machine learning motivated by reverse mathematics.
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.)