#
Homotopy Type Theory
entire relation > history (changes)

Showing changes from revision #1 to #2:
Added | ~~Removed~~ | ~~Chan~~ged

## Definition

< entire relation

~~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 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)$

~~
~~## See also

~~
~~
Last revised on June 15, 2022 at 20:52:01.
See the history of this page for a list of all contributions to it.