mathlib

34db3c34 - feat(order/category): various categories of ordered types (#3841)

feat(order/category): various categories of ordered types (#3841) This is a first step towards the category of simplicial sets (which are presheaves on the category of nonempty finite linear orders).