nLab opposite poset

Definition

Given a poset (or proset) $P$, its opposite (or dual, inverse, converse, reverse, etc), denoted $P^{op}$ (among other ways), is the poset (or proset) with the same underlying set, with $x \leq y$ in $P^op$ iff $y \leq x$ (equivalently, $x \geq y$) in the original $P$. We say that $\geq$ (the order relation in $P^op$ is the opposite order. This is a special case of both an opposite relation ($\geq$ compared to $\leq$) and an opposite category ($P^op$ compared to $P$).

In homotopy type theory

Given a preorder or (0,1)-category $P \coloneqq (F(P), \leq)$, an opposite preorder or opposite (0,1)-category is a preorder $P^\op \coloneqq (F(P), \geq)$ with $\geq$ defined as

$$a:F(P), b:F(P) \vdash a \geq b \coloneqq b \leq a$$

where $F$ is the forgetful functor that gets the underlying type for a preorder.

Related concepts

• preorder, poset

• opposite relation

• opposite magma

• opposite category

• antitone