|
|
|
|
|
|
by dmulligan
1545 days ago
|
|
|
> 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 |
|
|