Basic Category Theory in Lean This repository aims to reconstruct the contents of Tom Leinster's "Basic Category Theory" in Lean.