Partial functions

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-12-07.
Last modified on 2024-04-25.

module foundation.partial-functions where
Imports 
open import foundation.partial-elements
open import foundation.universe-levels

open import foundation-core.propositions

Idea

A partial function from A to B is a function from A into the type of partial elements of B. In other words, a partial function is a function

  A → Σ (P : Prop), (P → B).

Given a partial function f : A → B and an element a : A, we say that f is defined at a if the partial element f a of A is defined.

Partial functions can be described equivalently as morphisms of arrows

  ∅     1   ∅
  |     |   |
  |  ⇒  | ∘ |
  ∨     ∨   ∨
  A   Prop  B

where the composition operation is composition of polynomial endofunctors.

Definitions

Partial dependent functions

partial-dependent-function :
  {l1 l2 : Level} (l3 : Level) (A : UU l1) (B : A → UU l2) →
  UU (l1 ⊔ l2 ⊔ lsuc l3)
partial-dependent-function l3 A B =
  (x : A) → partial-element l3 (B x)

Partial functions

partial-function :
  {l1 l2 : Level} (l3 : Level) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3)
partial-function l3 A B = partial-dependent-function l3 A (λ _ → B)

The predicate on partial dependent functions of being defined at an element in the domain

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
  (f : partial-dependent-function l3 A B) (a : A)
  where

  is-defined-prop-partial-dependent-function : Prop l3
  is-defined-prop-partial-dependent-function =
    is-defined-prop-partial-element (f a)

  is-defined-partial-dependent-function : UU l3
  is-defined-partial-dependent-function =
    type-Prop is-defined-prop-partial-dependent-function

The predicate on partial functions of being defined at an element in the domain

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : partial-function l3 A B)
  (a : A)
  where

  is-defined-prop-partial-function : Prop l3
  is-defined-prop-partial-function =
    is-defined-prop-partial-dependent-function f a

  is-defined-partial-function : UU l3
  is-defined-partial-function =
    is-defined-partial-dependent-function f a

The partial dependent function obtained from a dependent function

module _
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x)
  where

  partial-dependent-function-dependent-function :
    partial-dependent-function lzero A B
  partial-dependent-function-dependent-function a =
    unit-partial-element (f a)

The partial function obtained from a function

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
  where

  partial-function-function : partial-function lzero A B
  partial-function-function = partial-dependent-function-dependent-function f

See also

Recent changes