Max Zeuner: A Cubical Approach to the Structure Identity Principle
Time: Wed 2020-02-19 10.00 - 11.45
Location: Kräftriket, house 5, room 16
Participating: Max Zeuner
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.)