nLab enriched setoid

Contents

Context

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

Enriched category theory

Analysis

Contents

Idea

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

Defintion

Let (M,,,1)(M, \leq, \otimes, 1) be a monoidal poset. A MM-enriched setoid or setoid 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 univalent setoid is an MM-enriched setoid which additinally satisfies 1o(a,b)a=b1 \leq o(a, b) \Rightarrow a = b.

For MM-enriched univalent setoids, 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.

Examples

See also

Last revised on May 30, 2022 at 20:50:42. See the history of this page for a list of all contributions to it.