nLab monoidal setoid

Context

Algebra

Category theory

Relations

Constructivism, Realizability, Computability

Contents

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.

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,)(A, \sim) with an element eAe \in A and a function m:A×AAm:A \times A \to A such that

  • mm preserves the equivalence relation: for all elements aAa \in A, bAb \in A, cAc \in A, and dAd \in A, if aca \sim c and bdb \sim d, then m(a,b)m(c,d)m(a, b) \sim m(c, d).

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

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

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

Examples

Monoidal setoid homomorphisms

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

  • ff preserves the equivalence relation: for all aAa \in A and bAb \in A, a Aba \sim_A b implies f(a) Bf(b)f(a) \sim_B f(b)

  • ff preserves the monoidal unit up to equivalence relation: f(e A) Be Bf(e_A) \sim_B e_B

  • ff preserves the monoidal product up to equivalence relation: for all aAa \in A and bAb \in A,

    f(m A(a,b)) Bm B(f(a),f(b))f(m_A(a, b)) \sim_B m_B(f(a), f(b))

Theorem

Let AA be a monoidal setoid, and let A/A / \sim be its quotient set. Then the function []:A(A/)[-]:A \to (A / \sim) which takes an element of AA 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.