Formalize closure properties of left orthogonal shapes and right orthogonal maps #81
Description
The notion of orthogonality from BW23 is formalized in #76.
It satisfies many desirable closure properties:
- In the left argument:
- isomorphism of shape-pairs
- composition
- left cancellation
- right cancellation with retraction
- pushout product
- crossing with a shape
- exact pushout
- retracts
- in the right argument:
- equivalence of maps
- composition
- right cancellation
- left cancellation with section
- exponentiation
- pullback
- retracts
- and many more
Metadata
Metadata
Assignees
Labels
No labels