Partial elements

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

Created on 2022-06-02.
Last modified on 2023-12-07.

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

open import foundation-core.propositions

Idea

A partial element of X consists of a proposition P and a map P → X. That is, the type of partial elements of X is defined to be

  Σ (P : Prop), (P → X).

We say that a partial element (P, f) is defined if the proposition P holds.

Alternatively, the type of partial elements of X can be descibed as the codomain of the composition

    1   ∅     ∅
    |   |     |
  T | ∘ |  =  |
    V   V     V
  Prop  X   P T X

of polynomial-endofunctors.md. Indeed, the codomain of this composition operation of morphisms is the polynomial endofunctor P T of the map T : 1 → Prop evaluated at X, which is exactly the type of partial elements of X.

Definitions

Partial elements of a type

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

module _
  {l1 l2 : Level} {X : UU l1} (x : partial-element l2 X)
  where

  is-defined-prop-partial-element : Prop l2
  is-defined-prop-partial-element = pr1 x

  is-defined-partial-element : UU l2
  is-defined-partial-element = type-Prop is-defined-prop-partial-element

The unit of the partial element operator

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

Properties

The type of partial elements is a directed complete poset

This remains to be shown. #734

See also

Recent changes