Homotopy Type Theory opposite preorder > history (Rev #2)

Contents

Definition

Given a preorder or (0,1)-precategory P(F(P),)P \coloneqq (F(P), \leq), an opposite preorder or opposite (0,1)-precategory 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

Revision on March 11, 2022 at 16:25:16 by Anonymous?. See the history of this page for a list of all contributions to it.