In a restriction category $\mathscr{C}$ each hom-set $\mathscr{C}(A,B)$ admits a partial order, where $f \leq g \iff f \approx g \circ f \downarrow$, I added this to Categories.Category.Restriction.Properties.Poset.
I've also removed the inner module in Categories.Category.Restriction.Properties and moved its parameters to the top-level module, such that using the lemmas is more convenient. This change is in a separate commit, so it can be easily be reverted if the old style is preferred.
In a restriction category $\mathscr{C}$ each hom-set $\mathscr{C}(A,B)$ admits a partial order, where $f \leq g \iff f \approx g \circ f \downarrow$, I added this to
Categories.Category.Restriction.Properties.Poset.I've also removed the inner module in
Categories.Category.Restriction.Propertiesand moved its parameters to the top-level module, such that using the lemmas is more convenient. This change is in a separate commit, so it can be easily be reverted if the old style is preferred.