|
|
|
|
|
|
by generalnonsense
1021 days ago
|
|
|
As others said above, `mathlib4` has quite a lot of Sheaf theory, and in particular the category of sheaves of Sets (i.e. Types) over an arbitrary site. In this sense, it is possible to talk about Grothendieck toposes. We don't have the characterization in terms of Giraud's axioms, though. |
|
|