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