Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 20:30 3a061790

View on Github →

refactor(category_theory): reverse simp lemmas about (co)forks (#13519) Makes fork.ι instead of t.π.app zero so that we avoid any unnecessary references to walking_parallel_pair in (co)fork homs. This induces quite a lot of changes in other files, but I think it's worth the pain. The PR also changes to avoid stating redundant morphisms.

Estimated changes