Showing changes from revision #0 to #1: Added | Removed | Changed

Contents

Whenever editing is allowed on the 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

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, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)