From 22214b8a04ff577cf09e60236ec99784116867a3 Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Thu, 23 Jun 2022 22:07:27 +0200
Subject: [PATCH] test adding agda page

---
 misc/wlpo.agda | 109 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 109 insertions(+)
 create mode 100644 misc/wlpo.agda

diff --git a/misc/wlpo.agda b/misc/wlpo.agda
new file mode 100644
index 0000000..2ff556a
--- /dev/null
+++ b/misc/wlpo.agda
@@ -0,0 +1,109 @@
+{-# 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))))