[[!redirects preordered type]] [[!redirects (0,1)-precategory]] #Contents# * table of contents {:toc} ## Definition ## A __preorder__ 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$. If $T$ comes with a preorder, then $T$ is a __preordered type__ or a __(0,1)-precategory__. ## Properties ## Every preordered type in a univalent universe is a [[set]] and a [[poset]]. ## See also ## * [[directed type]] * [[partial order]] * [[lattice]] * [[frame]] * [[total order]] * [[2-preorder]] ## References ## * Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis, The Univalence Principle ([abs:2102.06275](https://arxiv.org/abs/2102.06275)) * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)