Homotopy Type Theory enriched poset > history (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

 Defintion

< enriched poset

Let

MM be a meet-semilattice. A MM-enriched poset or poset enriched over/in MM is a type PP with

  • a function o:P×PMo:P \times P \to M called the order relation

  • a term

τ: a:P b:P c:Po(a,b)o(b,c)o(a,c)\tau:\prod_{a:P} \prod_{b:P} \prod_{c:P} o(a, b) \wedge o(b, c) \leq o(a, c)
  • a term
ι: a:Po(a,a)\iota:\prod_{a:P} \top \leq o(a, a)

Examples

  • A Lawvere metric space is a 0¯\overline{\mathbb{R}_{\geq 0}}-enriched poset, where 0¯\overline{\mathbb{R}_{\geq 0}} are the non-negative extended Dedekind real numbers.
  • A strictly ordered type is a Prop 𝒰 opProp_\mathcal{U}^\op-enriched poset, where Prop 𝒰 opProp_\mathcal{U}^\op is the opposite preorder of the type of propositions in a universe 𝒰\mathcal{U}.

See also

Last revised on June 9, 2022 at 23:20:47. See the history of this page for a list of all contributions to it.