mathlib

dbc03394 - feat(category_theory/limits/shapes/types): explicit isos (#13854)

feat(category_theory/limits/shapes/types): explicit isos (#13854) Requested on Zulip. https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Relating.20the.20categorical.20product.20and.20the.20normal.20product Co-authored-by: Scott Morrison <scott.morrison@gmail.com>