Re:With Category Theory, Mathematics Escapes from Equality (...
by dmulligan on Monday March 28, 2022 @08:23AM
(#30829713)
> 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.
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