# Homotopy Type Theory multivalued function > history (changes)

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

## 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)$