Homotopy Type Theory partial order > history (Rev #5, changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

Contents

Definition

A partial order on a type $T$ is a type family $(-)\leq(-)$ over $T$ with

• a family of dependent terms

$a:T, b:T \vdash \pi(a,b):isProp(a \leq b)$

representing that each type $a \leq b$ is a proposition.

• a family of dependent terms

$a:T \vdash \rho(a):a \leq a$

representing the reflexive property of $\leq$.

• a family of dependent terms

$a:T, b:T, c:T \vdash \tau(a, b, c):(a \leq b) \times (b \leq c) \to (a \leq c)$

representing the transitive property of $\leq$.

• a family of dependent terms

$a:T, b:T \vdash \sigma(a, b):(a \leq b) \times (b \leq a) \to (a = b)$

representing the anti-symmetric property of $\leq$.

If $T$ comes with a partial order, then $T$ is a partially ordered type. If $T$ is also a set, then $T$ is called a partially ordered set or poset. A poset is also a (0,1)-category.

Properties

Every partially ordered type in a univalent universe is a poset.