[[!redirects partially ordered type]] [[!redirects partially ordered set]] [[!redirects poset]] [[!redirects (0,1)-category]] < [[nlab:partial order]] #Contents# * table of contents {:toc} ## 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. ## See also ## * [[preorder]] * [[lattice]] * [[frame]] * [[total order]] * [[2-poset]] ## References ## * Ayberk Tosun, Formal Topology in Univalent Foundations [pdf](https://odr.chalmers.se/handle/20.500.12380/301098) * Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis, The Univalence Principle ([abs:2102.06275](https://arxiv.org/abs/2102.06275)) probably the HoT book as well, category: not redirected to nlab yet