mathlib

47861363 - feat(category_theory/limits): explicit isomorphisms between preserved limits (#3602)

feat(category_theory/limits): explicit isomorphisms between preserved limits (#3602) When `G` preserves limits, it's nice to be able to quickly obtain the iso `G.obj (pi_obj f) ≅ pi_obj (λ j, G.obj (f j))`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>