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