Homotopy Type Theory opposite preorder > history (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

<opposite preorder

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

Last revised on June 9, 2022 at 19:34:00. See the history of this page for a list of all contributions to it.