The weak limited principle of omniscience
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-08-08.
Last modified on 2023-06-08.
module foundation.weak-limited-principle-of-omniscience where
Imports
open import elementary-number-theory.natural-numbers open import foundation.disjunction open import foundation.negation open import foundation.universe-levels open import foundation-core.propositions open import foundation-core.sets open import univalent-combinatorics.standard-finite-types
Statement
The Weak Limited Principle of Omniscience asserts that for any sequence
f : ℕ → Fin 2
either f n = 0
for all n : ℕ
or not. In particular, it is a
restricted form of the law of excluded middle.
WLPO : UU lzero WLPO = (f : ℕ → Fin 2) → type-disj-Prop ( Π-Prop ℕ (λ n → Id-Prop (Fin-Set 2) (f n) (zero-Fin 1))) ( neg-Prop (Π-Prop ℕ (λ n → Id-Prop (Fin-Set 2) (f n) (zero-Fin 1))))
See also
- The principle of omniscience
- The limited principle of omniscience
- The lesser limited principle of omniscience
Recent changes
- 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497).