Total partial functions

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-12-07.
Last modified on 2024-01-14.

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

Recent changes