# Commit 2021-03-23 15:29 489f5225

View on Github →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`

.