The category of preorders.
Equations
@[protected, instance]
Equations
- Preorder.order_hom.category_theory.bundled_hom = {to_fun := order_hom.to_fun, id := order_hom.id, comp := order_hom.comp, hom_ext := order_hom.ext, id_to_fun := Preorder.order_hom.category_theory.bundled_hom._proof_1, comp_to_fun := Preorder.order_hom.category_theory.bundled_hom._proof_2}
@[protected, instance]
@[protected, instance]
Construct a bundled Preorder from the underlying type and typeclass.
Equations
@[protected, instance]
Equations
Constructs an equivalence between preorders from an order isomorphism between them.
Equations
- Preorder.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
order_dual
as a functor.
Equations
- Preorder.dual = {obj := λ (X : Preorder), Preorder.of (↥X)ᵒᵈ, map := λ (X Y : Preorder), ⇑order_hom.dual, map_id' := Preorder.dual._proof_1, map_comp' := Preorder.dual._proof_2}
@[simp]
The equivalence between Preorder
and itself induced by order_dual
both ways.
Equations
- Preorder.dual_equiv = category_theory.equivalence.mk Preorder.dual Preorder.dual (category_theory.nat_iso.of_components (λ (X : Preorder), Preorder.iso.mk (order_iso.dual_dual ↥X)) Preorder.dual_equiv._proof_1) (category_theory.nat_iso.of_components (λ (X : Preorder), Preorder.iso.mk (order_iso.dual_dual ↥X)) Preorder.dual_equiv._proof_2)
@[simp]
@[simp]
@[protected, instance]
@[protected, instance]
Equations
- Preorder_to_Cat.category_theory.full = {preimage := λ (X Y : Preorder) (f : Preorder_to_Cat.obj X ⟶ Preorder_to_Cat.obj Y), {to_fun := f.obj, monotone' := _}, witness' := Preorder_to_Cat.category_theory.full._proof_2}