A pain-free formalisation of the Leibniz construction

Nov 18 14:00 ₂₀₂₅

Abstract:For better or worse, some mathematicians working in formalisation (including myself) like to work in a proof-relevant setting, such as HoTT or simply MLTT without UIP. While theorems stated in these settings enjoy interpretations in a rich class of models, this matters little if we can't prove them. Indeed, even when proving the most innocent-looking theorems, there is one recurring issue that often stumps even the most seasoned formaliser: coherences. This talk is about my most recent visit to coherence hell and, in particular, a neat little trick that helped me and my collaborators escape it.

More specifically, this talk concerns an ongoing formalisation project with Tom de Jong and Nicolai Kraus on so-called Leibniz products and exponentials (also known as pushout products and pullback powers) and their adjointness. Although this problem is motivated by the development of simplicial type theory, it is also completely self-contained and should be understandable to anyone who knows some basic MLTT and/or category theory. The approach we've taken provides a heuristic for dealing with many coherence problems in general and my hope is that it will be useful to mathematicians and computer scientists stuck on similar problems.