[[!redirects total order]] [[!redirects linear order]] [[!redirects ordered type]] [[!redirects totally ordered type]] [[!redirects linearly ordered type]] [[!redirects ordered]] [[!redirects totally ordered]] [[!redirects linearly ordered]] ## Definition ## A [[partial order]] $\leq$ over a type $A$ is an __order__ (also called __total order__ or __linear order__) if it comes with a family of dependent terms $$a:A, b:A \vdash \tau(a, b): \Vert R(a, b) + R(b, a) \Vert$$ representing the totality condition for the partial order. $A$ is called an __ordered type__, __totally ordered type__, or __linearly ordered type__. ## See also ## * [[partial order]] * [[strict order]] * [[closed interval]] * [[simplex category]]