[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] A multivalued sequence on a type $T$ is a function $f:\mathbb{N} \to \mathcal{P}(T)$ such that for every natural number $n:\mathbb{N}$, $f(n)$ is an inhabited subset of $T$. By real number we mean modulated multivalued Cauchy real number. category: redirected to nlab