> It turns out that it is possible if you do it in a special way with locales What was special about it? From memory, the formalisation [1] proceeded exactly

> It turns out that it is possible if you do it in a special way with locales What was special about it? From memory, the formalisation [1] proceeded exactly how you would expect. Locales are simply an Isabelle mechanism (in addition to type classes) through which hierarchies of structures are built up. [1]: https://www.isa-afp.org/entries/Grothendieck_Schemes.html https://www.isa-afp.org/entries/Grothendieck_Schemes.html