Homotopy Type Theory multivalued function > history (Rev #2, changes)

The type of multivalued functions with domain $S$ and codomain $T$ in a universe $\mathcal{U}$, $S \to_\mathcal{U} T$, is defined as

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

See also

• entire relation
• partial function
• square root?