# Partial functions

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-12-07.

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