Homotopy Type Theory partial function > history (Rev #7, changes)

Showing changes from revision #6 to #7: Added | Removed | Changed

Definition

< partial function

Given types

SS and TT and a subtype DSD \subseteq S with inclusion? f:DSf:D \hookrightarrow S in a universe 𝒰\mathcal{U}, a partial 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 partial functions with domain SS and codomain TT in a universe 𝒰\mathcal{U}, S 𝒰TS \to_\mathcal{U} T, is defined as

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

A partial function could also be directly defined as a function f:ST f:S \to T_\bot, where T T_\bot is the partial function classifier of TT. The type of partial functions here is simply the function type ST S \to T_\bot.

Properties

Every partial function f:A 𝒰Bf:A \to_\mathcal{U} B between two sets AA and BB has an associated functional relation

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

See also

Revision on June 15, 2022 at 20:45:40 by Anonymous?. See the history of this page for a list of all contributions to it.