Basic category theory in Lean4?

Stream: lean4

[Daniel Donnelly]

I found this PDF one time of somoene making basic category theory proofs in Lean3. Is there one underway for Lean4? I can't find that PDF / article any more. How should one get started? My main goal is to have the user draw diagrams in Quiver and then the objects' / morphisms' Lean4 definitional code gets automatically generated.

[Scott Morrison]

The mathlib4 library has a substantial fraction of the mathlib3 category theory library already ported.

[Scott Morrison]

Certainly enough for your purposes.

[Daniel Donnelly]

Scott Morrison said:

Certainly enough for your purposes.

Are there articles on how to use it?

[Scott Morrison]

Are you asking about using Lean 4? The category theory library has essentially not changed at all, except that the language has moved underneath it.

[Daniel Donnelly]

Okay, then do you know of any Lean3 articles / books on category theory in particular?

[Kevin Buzzard]

Scott wrote a Lean 3 tutorial for LFTCM2020 -- it's on Thursday here https://github.com/leanprover-community/lftcm2020

[Kevin Buzzard]

And Scott and I at one point wrote a very basic markdown file just covering categories, functors and natural transformations IIRC -- the current version is here https://leanprover-community.github.io/theories/category_theory.html