mathlib3

ea74dc9f - feat(category_theory/limits): transport has_initial across equivalences (#15858)