{-# 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))))