## Definition ## Given [[set]]s $S$ and $T$ and a [[binary relation]] $\mapsto$, let us define a type family $$isEntire(S, T, \mapsto) \coloneqq \prod_{s:S} \Vert \sum_{t:T} s \mapsto t \Vert$$ $\mapsto$ is an __entire relation__ if there is a term $$p:isEntire(S, T, \mapsto)$$ The type of __entire relations__ 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_{\mapsto: S \times T \to Prop_\mathcal{U}} isEntire(S, T, \mapsto)$$ where $Prop_\mathcal{U}$ is the type of [[proposition]]s in $\mathcal{U}$. ## Properties ## Every [[multivalued function]] $f:A \to B$ between two sets $A$ and $B$ has an associated entire relation $$a:A \vdash p:a \mapsto f(a)$$ ## See also ## * [[binary relation]] * [[multivalued function]] * [[partial relation]]