11-12 March 2020, Ludwig-Maximilians-Universität München
| 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 |
| 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.) |