Topic: Olivia Caramello's work
Paul-Olivier Dehaye (Dec 13 2021 at 21:44):
Has anyone looked at the relevance of Olivia Caramello et al's work to Lean?
Paul-Olivier Dehaye (Dec 13 2021 at 22:15):
In particular I am curious about the link between the foundations question of @Valeria de Paiva to @Jeremy Avigad here and Caramello's description of "sites".
Bhavik Mehta (Dec 14 2021 at 04:57):
I've formalised a good amount of topos theory, but not her more recent stuff about bridges. We have sites in mathlib as well as sheaves on sites, and a more logic-focused development here: https://github.com/b-mehta/topos. As far as specific applications, I don't think there's anything more promising about her work in relation to Lean than any other category or topos theory research.
Last updated: Aug 03 2023 at 10:10 UTC