Internal language of geometric categories

Stream: general

[Fernando Chu]

Recently, there has been some renewed interest in using internal languages in Lean, e.g. here and here, so this is probably good time to share that we've finished formalizing the internal language of geometric categories!

The code for this is available in this repo. The formalization contains:

• A definition of geometric logic and its deduction rules. This is roughly intuitionistic first order logic extended with infinite joints, but without implications and foralls.
• An interpretation of any geometric logic formula into a geometric category.
• Soundness: Any derivation in geometric logic leads to a correct theorem of the corresponding interpretation in a geometric category.

Future work will include:

• Showing that Grothendieck topoi are geometric categories.
• Explore how the internal logic machinery can be used to prove things about the current Lean definitions of, e.g., sheaves of rings, sheaves of modules, schemes, etc.
• Explore if SynthLean or a similar mechanism can be used to reflect existing Lean proofs into the internal language.

Any feedback is very much appreaciated!

This is a joint project with @Kyod and @Yiming Xu. We thank the members of Loki and of this zulip for all their help.