binary_products): add some basic API for prod and coprod (#2396)

Commit

5 years ago

feat(category_theory/limits/shapes/binary_products): add some basic API for prod and coprod (#2396) Adding explicit proofs of some basic results about maps into A x B and maps from A coprod B

References

#2700 - Fix merge conflict

Author

kbuzzard

Parents

cf89963e

mathlib 01ac691d - feat(category_theory/limits/shapes/binary_products): add some basic API for prod and coprod (#2396)

mathlib
01ac691d - feat(category_theory/limits/shapes/binary_products): add some basic API for prod and coprod (#2396)