update

misc/wlpo.agda

@@ -1,109 +0,0 @@
-{-# OPTIONS --safe --without-K #-}
-
-open import Agda.Primitive renaming (Set to 𝒰)
-open import Agda.Builtin.Nat renaming (Nat to ℕ) hiding (_+_)
-open import Agda.Builtin.Bool renaming (Bool to 𝟚; false to 𝟘; true to 𝟙)
-open import Agda.Builtin.Equality using (_≡_; refl)
-open import Function using (_∘_; const)
-
-{- Variables -}
-variable
-  ₙ : Level
-  ₘ : Level
-  A : 𝒰 ₙ
-  B : 𝒰 ₙ
-  C : 𝒰 ₙ
-
-{- Types -}
-
-data ⊥ : 𝒰₀ where
-
-infixr 8 ¬_
-¬_ : 𝒰 ₙ → 𝒰 ₙ
-¬ p = p → ⊥
-
-infixr 2 _+_
-data _+_ (A : 𝒰 ₙ) (B : 𝒰 ₘ) : 𝒰 (ₙ ⊔ ₘ) where
-  inl : A → A + B
-  inr : B → A + B
-
-binary-sequence : 𝒰₀
-binary-sequence = ℕ → 𝟚  
-
-all-zeros : binary-sequence → 𝒰₀
-all-zeros α = (n : ℕ) → α n ≡ 𝟘
-
-has-WLPO : binary-sequence → 𝒰₀
-has-WLPO α = all-zeros α + ¬ (all-zeros α)   
-
-WLPO : 𝒰₀
-WLPO = (α : binary-sequence) → has-WLPO α   
-
-at-most-one-one : binary-sequence → 𝒰₀
-at-most-one-one α = (a b : ℕ) → α a ≡ 𝟙 → α b ≡ 𝟙 → a ≡ b
-
--- needed for LLPO
-dup : ℕ → ℕ
-dup 0 = 0
-dup (suc n) = suc (suc (dup n))
-
-evens : ℕ → ℕ
-evens = dup
-
-odds : ℕ → ℕ
-odds = suc ∘ dup
-
-LLPO : 𝒰₀
-LLPO = (α : binary-sequence) → at-most-one-one α → all-zeros (α ∘ evens) + all-zeros (α ∘ odds)
-
-{- Eliminators -}
-⊥-elim : ⊥ → A
-⊥-elim ()
-
-+-elim : A + B → (A → C) → (B → C) → C
-+-elim (inl a) f _ = f a
-+-elim (inr b) _ g = g b
-
--- A bit funky, but comes in handy
-𝟚-elim : (C : 𝟚 → 𝒰 ₙ) → (b : 𝟚) → (b ≡ 𝟘 → C 𝟘) → (b ≡ 𝟙 → C 𝟙) → C b
-𝟚-elim _ 𝟘 z _ = z refl
-𝟚-elim _ 𝟙 _ o = o refl
-
-{- Lemmas -}
-
--- I think this is a bit ugly, but it works and I'm tired
-e≢o : {n m : ℕ} → ¬ (evens n ≡ odds m)
-e≢o {zero} {zero} ()
-e≢o {zero} {suc m} ()
-e≢o {suc n} {zero} ()
-e≢o {suc n} {suc m} p = e≢o {n} {m} (ds (tr (he n) (ho m) p))
-  where
-    he : (q : ℕ) → evens (suc q) ≡ suc (suc (evens q))
-    he _ = refl
-
-    ho : (q : ℕ) → odds (suc q) ≡ suc (suc (odds q))
-    ho _ = refl
-
-    tr : ∀ {a b c d : ℕ} → a ≡ b → c ≡ d → a ≡ c → b ≡ d
-    tr refl refl refl = refl
-
-    ds : ∀ {q r : ℕ} → suc (suc q) ≡ suc (suc r) → q ≡ r
-    ds {zero} {zero} _ = refl
-    ds {suc q} {suc r} refl = refl
-
-
-lemma : (α : binary-sequence) → at-most-one-one α → ¬ all-zeros (α ∘ evens) → all-zeros (α ∘ odds)
-lemma α am11 na0e i = 𝟚-elim (_≡ 𝟘) ((α ∘ odds) i)
-                             (const refl)
-                             (λ p₁ → ⊥-elim (na0e (λ j → 𝟚-elim (_≡ 𝟘) ((α ∘ evens) j)
-                                                                (const refl)
-                                                                (λ p₂ → ⊥-elim (e≢o (am11 (evens j) (odds i) p₂ p₁))))))
-
-
-{- The main dish -}
-WLPO→LLPO : WLPO → LLPO
-WLPO→LLPO wlpo α am11 = +-elim (wlpo (α ∘ evens))
-                              inl
-                              (λ na0e → +-elim (wlpo (α ∘ odds))
-                                               inr
-                                               (λ na0o → ⊥-elim (na0o (lemma α am11 na0e))))