# Category of preorders #

This defines Preord, the category of preorders with monotone maps.

def Preord :
Type (u_1 + 1)

The category of preorders.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
def Preord.of (α : Type u_1) [] :

Construct a bundled Preord from the underlying type and typeclass.

Equations
Instances For
@[simp]
theorem Preord.coe_of (α : Type u_1) [] :
(Preord.of α) = α
Equations
instance Preord.instPreorderα (α : Preord) :
Preorder α
Equations
• α.instPreorderα = α.str
@[simp]
theorem Preord.Iso.mk_inv {α : Preord} {β : Preord} (e : α ≃o β) :
.inv = e.symm
@[simp]
theorem Preord.Iso.mk_hom {α : Preord} {β : Preord} (e : α ≃o β) :
.hom = e
def Preord.Iso.mk {α : Preord} {β : Preord} (e : α ≃o β) :
α β

Constructs an equivalence between preorders from an order isomorphism between them.

Equations
• = { hom := e, inv := e.symm, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem Preord.dual_map :
∀ {X Y : Preord} (a : X →o Y), Preord.dual.map a = OrderHom.dual a
@[simp]
theorem Preord.dual_obj (X : Preord) :

OrderDual as a functor.

Equations
Instances For

The equivalence between Preord and itself induced by OrderDual both ways.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem preordToCat_map :
∀ {X Y : Preord} (f : X Y), preordToCat.map f = .functor
@[simp]
theorem preordToCat_obj (X : Preord) :
preordToCat.obj X =

The embedding of Preord into Cat.

Equations
Instances For