#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$. Then the quotient set $S/\equiv$ is a set with a function $\iota \in {(S/\equiv)}^{S}$ such that $$\forall a \in S. \forall b \in S. (a \equiv b) \implies (\iota(a) = \iota(b))$$ ### In homotopy type theory ### Let $T$ be a type, and let $\equiv$ be an equivalence relation on $T$. 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 ## * [[Cauchy real numbers]] * [[generalized Cauchy real numbers]] * [[Eudoxus real numbers]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)