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


Given sets SS and TT and a binary relation \mapsto, let us define a type family

isEntire(S,T,) s:S t:TstisEntire(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,)p:isEntire(S, T, \mapsto)

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

S 𝒰T :S×TProp 𝒰isEntire(S,T,)S \to_\mathcal{U} T \coloneqq \sum_{\mapsto: S \times T \to Prop_\mathcal{U}} isEntire(S, T, \mapsto)

where Prop 𝒰Prop_\mathcal{U} is the type of propositions in 𝒰\mathcal{U}.


Every multivalued function f:ABf:A \to B between two sets AA and BB has an associated entire relation

a:Ap:af(a)a:A \vdash p:a \mapsto f(a)

See also

Revision on March 18, 2022 at 00:09:07 by Anonymous?. See the history of this page for a list of all contributions to it.