Total partial elements

Content created by Egbert Rijke.

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

module foundation.total-partial-elements where
Imports 
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

Recent changes