Olivia Caramello's work

Stream: general

[Paul-Olivier Dehaye]

Has anyone looked at the relevance of Olivia Caramello et al's work to Lean?

• https://www.oliviacaramello.com/Unification/HDRTalkOliviaCaramello.pdf
• https://preprints.ihes.fr/2016/M/M-16-26.pdf
• https://www.oliviacaramello.com/Unification/HDROliviaCaramello.pdf

[Paul-Olivier Dehaye]

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]

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.