Thomas Lamiaux: Univalent relational parametricity
Time: Wed 2022-04-06 10.00 - 12.00
Location: Kräftriket, House 5, Room 31
Participating: Thomas Lamiaux (Stockholm University)
The introduction of the axiom of Univalence gave content to the phrase "we identity isomorphic structure". Then it feels natural that if one proves a result on A which is equivalent to B then it also stands for B. However this is not automatic in HoTT\UF and requires a predicate P. It is technically possible in Cubical Agda, yet it is not trivial and can get quite involved. The seminar is about Univalent Relational Parametricity, which is a mixture of both Parametricity and Univalence that enables automatic transport of proofs.
During the first hour :
- The first part of the seminar will be an introduction on parametricity.
- The second will discuss the different ways to transport proofs and why this fails to be automated.
Focusing on the anticipation problemen and the computation problem.
The second hour and third part will be about the Univalent Relational Parametricity.
- Explaining Univalent Parametricity for CComega and explaining how it solves the anticipation and computation problem.
- Explaining Univalent Relational Parametricity and why it is much better setting by just a twist in the definition.
- Explaining how to extend Univalent Relational Parametricity to inductive types (nat, list ...) and to indexed inductive types (eq, vec...). Thus doing it for a great part of Coq.