nLab opposite poset


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

In homotopy type theory

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

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

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

See also

Last revised on June 9, 2022 at 23:33:21. See the history of this page for a list of all contributions to it.