Theorems · Definition · order theory

CategoryTheory.orderDualEquivalence

(X : Type u) → [inst : Preorder X] → Xᵒᵈ ≌ Xᵒᵖ

The equivalence of categories from the order dual of a preordered type X to the opposite category of the preorder X.

Defined in

Mathlib.CategoryTheory.Category.Preorder

Cited by

15 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Preorder