Category theory exercises

Stream: Copenhagen Masterclass 2023

[Kevin Buzzard]

I ported Scott Morrison's Lean 3 category theory exercises to Lean 4 and put them in the masterclass repo. See https://github.com/adamtopaz/CopenhagenMasterclass2023/tree/master/CategoryTheoryExercises . They would probably be good practice for someone who wants to learn how to do category theory in Lean 4.

[Julius Mann]

Kevin Buzzard said:

I ported Scott Morrison's Lean 3 category theory exercises to Lean 4 and put them in the masterclass repo. See https://github.com/adamtopaz/CopenhagenMasterclass2023/tree/master/CategoryTheoryExercises . They would probably be good practice for someone who wants to learn how to do category theory in Lean 4.

someone want to look at the excercises together?