Theorems · Definition · order theory

OrderHom.equivFunctor

{X : Type u} → {Y : Type v} → [inst : Preorder X] → [inst_1 : Preorder Y] → (X →o Y) ≃ CategoryTheory.Functor X Y

The equivalence between X →o Y and the type of functors X ⥤ Y between preorder categories X and Y.

Defined in

Mathlib.CategoryTheory.Category.Preorder

Cited by

2 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms

Assumes

PreorderPreorder