Homotopy Type Theory multivalued function > history (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed


< multivalued function

Given types

SS and TT and a type DD with effective epic function f:DSf:D \to S in a universe 𝒰\mathcal{U}, a multivalued function f:S 𝒰Tf:S \to_\mathcal{U} T with domain SS and codomain TT is simply a function f:DTf:D \to T.

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

S 𝒰T D:𝒰EffectiveEpic(D,S)×(DT)S \to_\mathcal{U} T \coloneqq \sum_{D:\mathcal{U}} EffectiveEpic(D, S) \times (D \to T)

where EffectiveEpic(D,S)EffectiveEpic(D, S) is the type of effective epic functions from DD to SS.


Every multivalued function f:A 𝒰Bf:A \to_\mathcal{U} 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

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