mathlib

b44e742e - feat(category_theory/limits): realise products as pullbacks (#14322)

feat(category_theory/limits): realise products as pullbacks (#14322) This was mostly done in #10581, this just adds the isomorphisms between the objects produced by the `has_limit` API. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>