Preorder-enriched Categories, Preorder-internal categories
I'm going to see how feasible it is to define these manually as structure on an existing category.
I'm going to see how feasible it is to define these manually as structure on an existing category.