Zulip Chat Archive

Stream: new members

Topic: category

Yono (Jul 30 2023 at 13:12):

How do I study how to write codes for category theory with mathlib? Are there guidebook with lean4?

Matthias Goerner (Jul 31 2023 at 07:30):

Did you see https://leanprover-community.github.io/theories/category_theory.html?

Matthias Goerner (Jul 31 2023 at 07:35):

I just noticed that this points to mathlib for lean3, not 4. This is for lean4: https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Category/Basic.html

Matthias Goerner (Jul 31 2023 at 07:39):

It would be helpful if there were examples. Can I define the category of groups in lean?

Yaël Dillies (Jul 31 2023 at 07:39):

docs#GroupCat

Last updated: Dec 20 2023 at 11:08 UTC