Commit 2021-03-23 15:29 489f5225

feat(category_theory/subobject): API for working with inequalities (#6818) This PR adds two types of declarations:

• Helper functions for showing that two subobjects are equal by giving a compatible isomorphism, and
• functions of_le/of_le_mk/of_mk_le/of_mk_le_mk that produce a morphism between the underlying objects from a proof of X ≤ Y. These are in essence just thin wrappers around underlying.map.