#Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ### ### In set theory ### 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 $$\forall a \in S. \forall b \in S. (a \equiv b) \implies (\iota(a) = \iota(b))$$ 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 $$\forall 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(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$. ### In homotopy type theory ### 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:T, b:T \vdash eq_{T/\equiv}(a, b): (a \equiv b) \to (\iota(a) =_{T/\equiv} \iota(b))$$ * a family of dependent terms $$a:T/\equiv, b:T/\equiv \vdash \tau(a, b): isProp(a =_{T/\equiv} b)$$ ## See also ## * [[setoid]] * [[rational numbers]] * [[decimal numbers]] * [[Cauchy real numbers]] * [[generalized Cauchy real numbers]] * [[Eudoxus real numbers]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)