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
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
. 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
Properties
The type of partial elements is a directed complete poset
This remains to be shown. #734
Recent changes
- 2023-09-10. Fredrik Bakke. Link issues to unfinished sections (#732).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-28. Fredrik Bakke. Enforce even indentation and automate some conventions (#635).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).