Partial elements

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-06-02.
Last modified on 2023-09-10.

module foundation.partial-elements where
open import foundation.dependent-pair-types
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.propositions


A partial element of X consists of a proposition P and a map P → X. We say that a partial element (P, f) is defined if the proposition P holds.

partial-element : {l1 : Level} (l2 : Level)  UU l1  UU (l1  lsuc l2)
partial-element l2 X = Σ (Prop l2)  P  type-Prop P  X)

is-defined-partial-element-Prop :
  {l1 l2 : Level} {X : UU l1} (x : partial-element l2 X)  Prop l2
is-defined-partial-element-Prop x = pr1 x

is-defined-partial-element :
  {l1 l2 : Level} {X : UU l1} (x : partial-element l2 X)  UU l2
is-defined-partial-element x = type-Prop (is-defined-partial-element-Prop x)

unit-partial-element :
  {l1 l2 : Level} {X : UU l1}  X  partial-element lzero X
pr1 (unit-partial-element x) = unit-Prop
pr2 (unit-partial-element x) y = x


The type of partial elements is a directed complete poset

This remains to be shown. #734

Recent changes