4 ms·
We don't have any topos theory, that's right. But all the prerequisites are there. If you're interested in working on it I strongly suggest to ask on Zulip.
by riccardobrasca 3y ago
We don't have any topos theory, that's right. But all the prerequisites are there. If you're interested in working on it I strongly suggest to ask on Zulip.
- kevinbuzzard 3y agoHere's a Lean 3 development of a bunch of topos theory https://github.com/b-mehta/topos/tree/master/src https://github.com/b-mehta/topos/tree/master/src , but it's not in the maths library (and now needs to be updated to Lean 4, although the community have had great success with that kind of project; one million lines of mathlib was translated from Lean 3 to Lean 4 using a combination of automation and human work)