Formalizing Lawvere Duality

Stream: new members

[Sudhir Murthy]

Hey! Under the guidance of a mentor, I am working together with a group of other undergraduates in an attempt to formalize Lawvere Duality in Lean, on the biequivalence between 2-categories Alg and FP.
(We are new to Lean and Category Theory, but we have an incredible mentor!)

Is it advisable we begin the project in Lean 4 instead of Lean 3?
Are there tutorials or documentation for helpful category-theory-specific tactics?

[Johan Commelin]

@Sudhir Murthy Welcome! There's been a lot of progress on category theory in Lean 4 recently. Do you have a deadline for this project? If the deadline is within 2 months, it might be wise to stick to Lean 3. Otherwise, I think it might be a good idea to give Lean 4 a shot.

[Johan Commelin]

There is one helpful category-theory-specific tactic: tidy (aka obviously) in Lean 3 and aesop_cat in Lean 4.

[Adam Topaz]

I'm quite sure we have all the prereqs that are needed for Lawvere duality already ported to mathlib4.

[Sudhir Murthy]

Thank you both very much! We have a deadline of 9 weeks but it's okay if we don't finish the project.
I'll pass this information to the team; I think we'll give Lean 4 a shot.