Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
Given a set $S$ and an equivalence relation $\equiv$ on $S$, the quotient set of $S$ by $\equiv$ is the set $S/{\equiv}$ whose elements are the elements of $S$ but where two elements are now considered equal if in $S$ they were merely equivalent.
If changing the definition of equality like this is not allowed in your foundations of mathematics, then you can still define $S/{\equiv}$ as a subset of the power set of $S$ as follows:
If you don't have (extensional) power sets either, then you'll have to use setoids (in which case, perhaps you'd do better to change your terminology as described there). Alternatively, don't worry about any of this and just include the existence of quotient objects in Set as an axiom (the axiom of quotient sets, which you have if you assume that $\Set$ is a pretopos or a Grothendieck topos as given by Giraud's axioms). There are actually two possible axiom of quotient sets, depending on what definition of relation one uses.
The weaker version of the axiom of quotient sets is the one which states that the coherent category $Set$ is a pretopos: that every internal equivalence relation on a set $A$, defined as a subset $\equiv$ of the Cartesian product $A \times A$ satisfying reflexivity, transitivity, and symmetry, has a quotient set $A/\equiv$.
The stronger version of the axiom of quotient sets states that every proposition $x \equiv y$ in the context of the variables $x \in A$ and $y \in A$ which satisfies reflexivity, transitivity, and symmetry has a quotient set $A/\equiv$. In some presentations of set theory, this is an axiom schema of quotient sets.
In any case, the element of $S/{\equiv}$ that comes from the element $x$ of $S$ may be denoted $[x]_{\equiv}$, or simply $[x]$ if ${\equiv}$ is understood, or simply $x$ if there will be no confusion as to which set it is an element of. This $[x]$ is called the equivalence class of $x$ with respect to $\equiv$; the term ‘class’ here is an old word for ‘set’ (in the sense of ‘subset’) and refers to the definition (1) above, where $[x]$ is literally the set $A$.
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 S \to A$ such that for all $a \in S$ and $b \in S$, $(a \equiv b)$ implies $(\iota(a) = \iota(b))$.
A quotient set algebra homomorphism of $S$ and $\equiv$ is a function $f: A \to B$ between two quotient set algebras $A$ and $B$ such that for all $a \in S$, $f(\iota_A(a)) = \iota_B(a)$.
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(A, B)$ for $A \in Ob(QSA(S, \equiv))$ and $B \in Ob(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 symmetric proset. The quotient set $T/\equiv$ is a higher inductive type inductively generated by the following:
a function $\iota: T \to T/\equiv$
a family of dependent terms
a family of dependent terms
The axiom of quotient sets in type theory says that every symmetric proset is a set.
Quotient sets in Set generalise to quotient objects in other categories. In particular, an exact category is a regular category in which every congruence on every object has an effective quotient object.
Last revised on December 21, 2022 at 02:35:05. See the history of this page for a list of all contributions to it.