nLab enriched set



(0,1)(0,1)-Category theory

Enriched category theory




Recall (here) that a set may be understood as a thin univalent (0,1)-dagger category, hence as a thin univalent dagger-category enriched over the cartesian monoidal proset of truth values. In generalization, one may speak of enriching preorders over other monoidal posets.


Let (M,,,1)(M, \leq, \otimes, 1) be a monoidal poset. A MM-enriched symmetric proset or symmetric proset enriched over/in MM is a set PP with a binary function o:P×PMo:P \times P \to M such that

  • for every aPa \in P, bPb \in P, and cPc \in P, o(a,b)o(b,c)o(a,c)o(a, b) \otimes o(b, c) \leq o(a, c)

  • for every aPa \in P and bPb \in P, o(a,b)o(b,a)o(a, b) \leq o(b, a)

  • for every aPa \in P, 1o(a,a)1 \leq o(a, a)

An MM-enriched set or set enriched over/in MM is an MM-enriched symmetric proset which additinally satisfies 1o(a,b)a=b1 \leq o(a, b) \Rightarrow a = b.

For MM-enriched sets, o(a,b)=o(b,a)o(a, b) = o(b, a), o(a,a)=1o(a, a) = 1, and 1=o(a,b)a=b1 = o(a, b) \Rightarrow a = b.


See also

Last revised on September 22, 2022 at 19:10:54. See the history of this page for a list of all contributions to it.