Welcome!

The is the documentation site for a formalization of categorical logic in the Lean 3 theorem prover, currently being worked on by Jacob Neumann. This formalization will generally follow these notes, written by Steve Awodey and Andrej Bauer.

This site is constantly a work in progress and will change frequently, so check back in. If you're interested in contributing, please email Jacob or open an issue or pull request at the formalization Github repository!