symmetric monoidal (∞,1)-category of spectra
Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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.
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)$.
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.
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$,
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.
Last revised on July 10, 2024 at 18:38:54. See the history of this page for a list of all contributions to it.