Homotopy Type Theory entire relation > history (Rev #1)

Definition

Given sets $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 propositions 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)$