Zulip Chat Archive

Stream: general

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