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 group. Equivalently, a locally thin 2-group, or in foundations where 2-categories are locally univalent by default, a locally thin pre-2-group. Also, equivalently, a monoidal setoid in which the monoidal product with any element has an inverse up to equivalence relation.
“Groupal setoid”, “groupal Bishop set”, and “Bishop group” 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 groupal setoid, groupal Bishop set, or Bishop group is a monoidal setoid with a function such that
preserves the equivalence relation: for all elements and , if , then .
satisfies the left and right inverse laws up to the equivalence relation: for all elements , and .
is abelian groupal or symmetric groupal or braided groupal if additionally for all elements and , .
The set of functions from the boolean domain to the natural numbers , equipped with the equivalence relation , is an abelian groupal setoid.
Given any Archimedean ordered field , the set of Cauchy sequences in is an abelian groupal setoid.
Given any Archimedean ordered field , the set of all locators of all elements of is an abelian groupal setoid.
Given two abelian groups and , the free abelian group of the product of the carrier sets of and , equipped with the equivalence relation generated by
for all and and
for all and , is an abelian groupal setoid whose quotient set is the tensor product of abelian groups .
Last revised on July 10, 2024 at 18:38:28. See the history of this page for a list of all contributions to it.