This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The lesser limited principle of omniscience

module foundation.lesser-limited-principle-of-omniscience where
Imports 
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.parity-natural-numbers

open import foundation.disjunction
open import foundation.universe-levels

open import foundation-core.fibers-of-maps
open import foundation-core.propositions
open import foundation-core.sets

open import univalent-combinatorics.standard-finite-types

Statement

The lesser limited principle of omniscience asserts that for any sequence f : ℕ → Fin 2 containing at most one 1, either f n ＝ 0 for all even n or f n ＝ 0 for all odd n.

LLPO : UU lzero
LLPO =
  (f : ℕ → Fin 2) → is-prop (fiber f (one-Fin 1)) →
  type-disjunction-Prop
    ( Π-Prop ℕ
      ( λ n →
        function-Prop (is-even-ℕ n) (Id-Prop (Fin-Set 2) (f n) (zero-Fin 1))))
    ( Π-Prop ℕ
      ( λ n →
        function-Prop (is-odd-ℕ n) (Id-Prop (Fin-Set 2) (f n) (zero-Fin 1))))

See also