The category of preorders.

Equations

• Preorder = category_theory.bundled preorder

Equations

• Preorder.category_theory.bundled_hom = {to_fun := preorder_hom.to_fun, id := preorder_hom.id, comp := preorder_hom.comp, hom_ext := preorder_hom.coe_inj, id_to_fun := Preorder.category_theory.bundled_hom._proof_1, comp_to_fun := Preorder.category_theory.bundled_hom._proof_2}

Construct a bundled Preorder from the underlying type and typeclass.

Equations

• Preorder.of α = category_theory.bundled.of α

Equations

• Preorder.inhabited = {default := Preorder.of punit directed_order.to_preorder}

Equations

• α.preorder = α.str