Categorical logic...

We use the ideas and tools of category theory to investigate formal languages and deductive calculi

...formalized in Lean!

Our definitions and proofs are expressed in the Lean proof assistant, so we can be sure they're completely correct