nLab monoidal setoid

1. Idea

A setoid or Bishop set whose quotient set is a monoid. Equivalently, a thin monoidal groupoid, or in foundations where groupoids are univalent by default, a thin monoidal pregroupoid.

“Monoidal setoid”, “monoidal Bishop set”, and “Bishop monoid” are placeholder names for a concept which may or may not have another name in the mathematics literature.

2. Definition

Here we assume that setoids or Bishop sets are equipped with an equivalence relation (rather than a pseudo-equivalence relation). A monoidal setoid or monoidal Bishop set or Bishop monoid is a setoid $(A, \sim)$ with an element $e \in A$ and a function $m:A \times A \to A$ such that

• $m$ preserves the equivalence relation: for all elements $a \in A$, $b \in A$, $c \in A$, and $d \in A$, if $a \sim c$ and $b \sim d$, then $m(a, b) \sim m(c, d)$.

• $m$ is associative up to the equivalence relation: for all elements $a \in A$, $b \in A$, $c \in A$, $m(a, m(b, c)) \sim m(m(a, b), c)$

• $m$ is left and right unital up to the equivalence relation: for all elements $a \in A$, $m(a, e) \sim a$ and $m(e, a) \sim e$.

$A$ is commutative monoidal or symmetric monoidal or braided monoidal if additionally for all elements $a \in A$ and $b \in A$, $m(a, b) \sim m(b, a)$.

3. Examples

• The set $\mathbb{N}^\mathbb{2}$ of functions from the boolean domain $\mathbb{2}$ to the natural numbers $\mathbb{N}$, equipped with the equivalence relation $f \sim g \coloneqq f(0) + g(1) = f(1) + g(0)$, is a monoidal setoid.

• Given any Archimedean ordered field $F$, the set of Cauchy sequences in $F$ is a monoidal setoid.

• Given any Archimedean ordered field $F$, the set of all locators of all elements of $F$ is a monoidal setoid.

• The quotient set of any monoidal setoid by its equivalence relation is a monoidal setoid where the equivalence relation is given by equality

• More generally, any monoid is a monoidal setoid in which the equivalence relation is given by equality.

4. Monoidal setoid homomorphisms

A monoidal setoid homomorphism between two monoidal setoids $A$ and $B$ is a function $h:A \to B$ such that

• $f$ preserves the equivalence relation: for all $a \in A$ and $b \in A$, $a \sim_A b$ implies $f(a) \sim_B f(b)$

• $f$ preserves the monoidal unit up to equivalence relation: $f(e_A) \sim_B e_B$

• $f$ preserves the monoidal product up to equivalence relation: for all $a \in A$ and $b \in A$,

  $$f(m_A(a, b)) \sim_B m_B(f(a), f(b))$$

Theorem 4.1. Let $A$ be a monoidal setoid, and let $A / \sim$ be its quotient set. Then the function $[-]:A \to (A / \sim)$ which takes an element of $A$ to its equivalence class is a monoidal setoid homomorphism.

5. Related concepts

• setoid

• monoid

• groupal setoid

• ring setoid

• monoidal category

• A-monoid