Category of preorders
@[instance]
def
preorder_hom.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β] :
has_coe_to_fun (preorder_hom α β)
Equations
- preorder_hom.has_coe_to_fun = {F := λ (f : preorder_hom α β), α → β, coe := preorder_hom.to_fun _inst_2}
@[ext]
theorem
preorder_hom.ext
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(f g : preorder_hom α β) :
theorem
preorder_hom.coe_inj
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(f g : preorder_hom α β) :
@[simp]
The identity function as bundled monotone function.
@[instance]
Equations
- preorder_hom.inhabited = {default := preorder_hom.id _inst_1}
@[simp]
@[simp]
theorem
preorder_hom.comp_to_fun
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[preorder α]
[preorder β]
[preorder γ]
(g : preorder_hom β γ)
(f : preorder_hom α β)
(a : α) :
def
preorder_hom.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[preorder α]
[preorder β]
[preorder γ] :
preorder_hom β γ → preorder_hom α β → preorder_hom α γ
The composition of two bundled monotone functions.
@[simp]
theorem
preorder_hom.comp_id
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(f : preorder_hom α β) :
f.comp preorder_hom.id = f
@[simp]
theorem
preorder_hom.id_comp
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(f : preorder_hom α β) :
preorder_hom.id.comp f = f
@[instance]
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
@[instance]