Showing changes from revision #4 to #5:
Added | Removed | Changed
Whenever editing is allowed on the nLab again, this article should be ported over there.
Let $S$ be a set and let $\equiv$ be an equivalence relation on $S$. Let us define a quotient set algebra of $S$ and $\equiv$ to be a set $A$ with a function $\iota \in A^S$ such that
A quotient set algebra homomorphism of $S$ and $\equiv$ is a function $f \in B^A$ between two quotient set algebras $A$ and $B$ such that
The category of quotient set algebras of $S$ and $\equiv$ is the category $QSA(S, \equiv)$ whose objects $Ob(QSA(S, \equiv))$ are quotient set algebras of $S$ and $\equiv$ and whose morphisms $Mor(QSA(S, \equiv))$ are quotient set algebra homomorphisms of $S$ and $\equiv$. The quotient set of $S$ and $\equiv$, denoted $S/\equiv$, is defined as the initial object in the category of quotient set algebras of $S$ and $\equiv$.
Let $(T,\equiv)$ be a setoid. The quotient set $T/\equiv$ is inductively generated by the following:
a function $\iota: T \to T/\equiv$
a family of dependent terms
a family of dependent terms
Last revised on June 15, 2022 at 20:37:40. See the history of this page for a list of all contributions to it.