Homotopy Type Theory entire relation > history (Rev #2, changes)

$\mapsto$ is an entire relation if there is a term

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

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

See also

• binary relation
• multivalued function
• partial relation?