## Defintion ## Let $M$ be a [[meet-semilattice]]. A **$M$-enriched poset** or **poset enriched over/in $M$** is a type $P$ with * a function $o:P \times P \to M$ called the **order relation** * a term $$\tau:\prod_{a:P} \prod_{b:P} \prod_{c:P} o(a, b) \wedge o(b, c) \leq o(a, c)$$ * a term $$\iota:\prod_{a:P} \top \leq o(a, a)$$ ## Examples ## * A Lawvere metric space is a $\overline{\mathbb{R}_{\geq 0}}$-enriched poset, where $\overline{\mathbb{R}_{\geq 0}}$ are the non-negative extended Dedekind real numbers. * A [[strictly ordered type]] is a $Prop_\mathcal{U}^\op$-enriched poset, where $Prop_\mathcal{U}^\op$ is the [[opposite preorder]] of the type of [[proposition]]s in a universe $\mathcal{U}$. ## See also ## * [[meet-semilattice]] * [[Lawvere metric space]] * [[strict order]]