## Definition ## Given types $S$ and $T$ and a type $D$ with [[effective epic function]] $f:D \to S$ in a universe $\mathcal{U}$, a __multivalued function__ $f:S \to_\mathcal{U} T$ with __domain__ $S$ and __codomain__ $T$ is simply a function $f:D \to T$. The type of __multivalued functions__ with domain $S$ and codomain $T$ in a universe $\mathcal{U}$, $S \to_\mathcal{U} T$, is defined as $$S \to_\mathcal{U} T \coloneqq \sum_{D:\mathcal{U}} EffectiveEpic(D, S) \times (D \to T)$$ where $EffectiveEpic(D, S)$ is the type of effective epic functions from $D$ to $S$. ## Properties ## Every multivalued function $f:A \to_\mathcal{U} B$ between two sets $A$ and $B$ has an associated [[entire relation]] $$a:A \vdash p:a \mapsto f(a)$$ ## See also ## * [[entire relation]] * [[partial function]] * [[square root]]