Lean[0]'s mathlib has quite nice formalisation of category theory[1] with plenty examples of concrete categories even sheaves and toposes. [0] https://leanprov

Lean[0]'s mathlib has quite nice formalisation of category theory[1] with plenty examples of concrete categories even sheaves and toposes. [0] https://leanprover.github.io/programming_in_lean/#01_Introduction.html https://leanprover.github.io/programming_in_lean/#01_Introdu... [1] https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/category/default.lean#L92 https://github.com/leanprover-community/mathlib/blob/master/...