Topos theory in lean

Stream: mathlib4

[Colby Brown]

Hello, I have been working through "Sheaves in Geometry and Logic" by Mac Lane and Moerdijk in Lean and I have finished proving that every topos is cartesian closed, theorem IV.2.1. I have not seen topos theory in lean before so I am wondering if this would be a good addition to mathlib. My code is here: https://github.com/colbyaustinbrown/sigal/blob/main/Sigal/Chapter4/Basic.lean, it will need a bit of work to make it more readable and mathlib style guide compliant, but I am wondering if there is any desire for this code in mathlib or other advice about this project.

[Kevin Buzzard]

@Bhavik Mehta

[Adrian Marti]

See this for logical aspects of topos theory (I'm currently thinking about how to do terms in a pretty general setting).

[Adrian Marti]

There is also a partial port of Bhavik Mehta's topos theory repository in Lean 3 here, related to a thesis project at the university of Bonn.