## Definition ## Given types $S$ and $T$ and a [[subtype]] $D \subseteq S$ with [[inclusion]] $f:D \hookrightarrow S$ in a universe $\mathcal{U}$, a __partial function__ $f:S \to_\mathcal{U} T$ with __domain__ $S$ and __codomain__ $T$ is simply a function $f:D \to T$. The type of __partial 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}} (D \subseteq S) \times (D \to T)$$ A __partial function__ could also be directly defined as a function $f:S \to T_\bot$, where $T_\bot$ is the [[partial function classifier]] of $T$. The type of partial functions here is simply the function type $S \to T_\bot$. ## Properties ## Every partial function $f:A \to_\mathcal{U} B$ between two sets $A$ and $B$ has an associated [[functional relation]] $$a:A \vdash p:a \mapsto f(a)$$ ## See also ## * [[functional relation]] * [[partial function classifier]] * [[multivalued function]] * [[category of partial functions in a set]] * [[polynomial function]] * [[reciprocal function]] * [[rational function]] * [[principal square root]]