# Total partial functions

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-12-07.

module foundation.total-partial-functions where

Imports
open import foundation.dependent-pair-types
open import foundation.partial-functions
open import foundation.universe-levels

open import foundation-core.propositions


## Idea

A partial function f : A → B is said to be total if the partial element f a of B is defined for every a : A. The type of total partial functions from A to B is equivalent to the type of functions from A to B.

## Definitions

### The predicate of being a total partial function

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

is-total-prop-partial-function : Prop (l1 ⊔ l3)
is-total-prop-partial-function =
Π-Prop A (is-defined-prop-partial-function f)

is-total-partial-function : UU (l1 ⊔ l3)
is-total-partial-function = type-Prop is-total-prop-partial-function


### The type of total partial functions

total-partial-function :
{l1 l2 : Level} (l3 : Level) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3)
total-partial-function l3 A B =
Σ (partial-function l3 A B) is-total-partial-function