mathlib3

3a061790 - refactor(category_theory): reverse simp lemmas about (co)forks (#13519)

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 `fork.is_limit.mk` to avoid stating redundant morphisms.