This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Total partial elements

module foundation.total-partial-elements where

open import foundation.dependent-pair-types
open import foundation.partial-elements
open import foundation.universe-levels

Idea

A partial element a of A is said to be total^¶ if it is defined. The type of total partial elements of A is equivalent to the type A.

Definitions

The type of total partial elements

total-partial-element :
  {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2)
total-partial-element l2 A =
  Σ (partial-element l2 A) is-defined-partial-element