CantorNormalForm.LimitsAndTaboos

----------------------------------------------------------------------------------------------------
-- Some taboos about Cnf having limits of bounded sequences
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

module CantorNormalForm.LimitsAndTaboos where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Data.Sum as Sum
open import Cubical.Data.Empty
  renaming (rec to ⊥-rec)
open import Cubical.Relation.Nullary
open import Cubical.Data.Nat as N
  using (ℕ ; suc ; injSuc)
open import Cubical.Data.Nat.Order as N using ()
open import Cubical.Data.Bool
  renaming (false to ff; true to tt)
  hiding (_≤_; _≥_)


open import PropTrunc
open import General-Properties
open import CantorNormalForm.Base
open import CantorNormalForm.Wellfoundedness
open import CantorNormalForm.Classifiability
open import CantorNormalForm.Addition
open import CantorNormalForm.Subtraction

open import BooleanSequence
open import Simulations Cnf _≤_

--
-- We have showed that Cnf does not have limits.
--
import CantorNormalForm.Classifiability
  using (Cnf-does-not-have-limits)


--
-- Assuming LEM, every nonempty subset of CNFs has a minimal element.
-- (A consequence of Theorem 10.4.3 in the HoTT book)
--
minimal-witness : LEM → (P : Cnf → Type) → (∀ x → isProp (P x))
  → ∀ x → P x → Σ[ a ∈ Cnf ] P a × (∀ z → P z → a ≤ z)
minimal-witness lem P pvP = wf-ind step
 where
  A Q : Cnf → Type
  A x = ∀ z → P z → x ≤ z
  Q x = P x → Σ[ y ∈ Cnf ] P y × A y
  pvA : ∀ x → isProp (A x)
  pvA x = isPropΠ2 (λ _ _ → isProp⟨≤⟩)
  pvPA : ∀ x → isProp (P x × A x)
  pvPA x = isProp× (pvP x) (pvA x)
  ΣPA-isProp : isProp (Σ[ y ∈ Cnf ] P y × A y)
  ΣPA-isProp (y₀ , py₀ , ay₀) (y₁ , py₁ , ay₁) = Σ≡Prop pvPA y₀≡y₁
   where
    y₀≤y₁ : y₀ ≤ y₁
    y₀≤y₁ = ay₀ y₁ py₁
    y₁≤y₀ : y₁ ≤ y₀
    y₁≤y₀ = ay₁ y₀ py₀
    y₀≡y₁ : y₀ ≡ y₁
    y₀≡y₁ = ≤-antisym y₀≤y₁ y₁≤y₀
  step : ∀ x → (∀ y → y < x → Q y) → Q x
  step x h px with lem (A x) (pvA x)
  ... | yes a = x , px , a
  ... | no ¬a = ∥-∥rec ΣPA-isProp claim₁ claim₀
   where
    claim₀ : ∥ Σ[ z ∈ Cnf ] ¬ (P z → x ≤ z) ∥
    claim₀ = LEM-¬∀-∃¬ _ (λ z → isPropΠ (λ _ → isProp⟨≤⟩)) lem ¬a
    claim₁ : (Σ[ z ∈ Cnf ] ¬ (P z → x ≤ z)) → Σ[ y ∈ Cnf ] P y × A y
    claim₁ (z , f) = goal
     where
      z<x : z < x
      z<x with <-tri z x
      ... | inl z<x = z<x
      ... | inr z≥x = ⊥-rec (f (λ _ → z≥x))
      pz : P z
      pz with lem (P z) (pvP z)
      ... | yes p = p
      ... | no ¬p = ⊥-rec (f λ p → ⊥-rec (¬p p))
      goal : Σ[ y ∈ Cnf ] P y × A y
      goal = h z z<x pz


--
-- Therefore, assuming LEM, we can compute suprema of bounded sequences.
--
LEM-computes-sup : LEM
  → (f : ℕ → Cnf) (b : Cnf) → (∀ i → f i ≤ b)
  → Σ[ a ∈ Cnf ] a is-sup-of f
LEM-computes-sup lem f = minimal-witness lem P pvP
 where
  P : Cnf → Type
  P b = ∀ i → f i ≤ b
  pvP : ∀ b → isProp (P b)
  pvP _ = isPropΠ (λ _ → isProp⟨≤⟩)

--
-- If Cnf has limits of bounded increasing sequences, then WLPO holds.
-- The proof is essentially the same as the one of the no go theorem.
--

-- We first specialise the jumping sequence s ↑ to CNF

_↑ : (ℕ → Bool) → ℕ → Cnf
(s ↑)  0      = 𝟎
(s ↑) (suc i) = if (least-index-true s i) then ω else ((s ↑) i + 𝟏)

s↑-spec-<ω : ∀ s → (n : ℕ) → (∀ i → i N.< n → s i ≡ ff) → (s ↑) n < ω
s↑-spec-<ω s 0 p = <₁
s↑-spec-<ω s (suc n) p = goal
   where
    claim₀ : ∀ i → i N.≤ n → s i ≡ ff
    claim₀ i i≤n = p i (N.suc-≤-suc i≤n)
    claim₁ : least-index-true s n ≡ ff
    claim₁ = least-index-true-spec-ff s n claim₀
    claim₂ : (s ↑) (suc n) ≡ (s ↑) n + 𝟏
    claim₂ = cong (if_then ω else (s ↑) n + 𝟏) claim₁
    IH : (s ↑) n < ω
    IH = s↑-spec-<ω s n (λ i i<n → p i (N.≤-suc i<n))
    claim₃ : (s ↑) n + 𝟏 < ω
    claim₃ = ω^-is-add-indecomposable ((s ↑) n) 𝟏 IH (<₂ <₁)
    goal : (s ↑) (suc n) < ω
    goal = subst (_< ω) (sym claim₂) claim₃

s↑-inc : ∀ s → is-<-increasing (s ↑)
s↑-inc s i with least-index-true s i ≟ tt
... | yes p = subst ((s ↑) i <_) (sym claim₀) claim₁
   where
    claim₀ : (s ↑) (suc i) ≡ ω
    claim₀ = cong (if_then ω else ((s ↑) i + 𝟏)) p
    q : ∀ j → j N.< i → s j ≡ ff
    q = least-index-true-case-tt s i p
    claim₁ : (s ↑) i < ω
    claim₁ = s↑-spec-<ω s i q
... | no ¬p = goal
   where
    p : least-index-true s i ≡ ff
    p = ¬true→false _ ¬p
    claim₀ : (s ↑) (suc i) ≡ (s ↑) i + 𝟏
    claim₀ = cong (if_then ω else ((s ↑) i + 𝟏)) p
    claim₁ : (s ↑) i < (s ↑) i + 𝟏
    claim₁ = <+𝟏
    goal : (s ↑) i < (s ↑) (suc i)
    goal = subst ((s ↑) i <_) (sym claim₀) claim₁

s↑-inc' : ∀ s → (i j : ℕ) → i N.< j → (s ↑) i < (s ↑) j
s↑-inc' s i 0 i<0 = ⊥-rec (N.¬-<-zero i<0)
s↑-inc' s i (suc j) (0 , i+1≡j+1) = subst (λ x → (s ↑) i < (s ↑) x) i+1≡j+1 (s↑-inc s i)
s↑-inc' s i (suc j) (suc k , k+i+1≡j) = <-trans IH fact
   where
    IH : (s ↑) i < (s ↑) j
    IH = s↑-inc' s i j (k , injSuc k+i+1≡j)
    fact : (s ↑) j < (s ↑) (suc j)
    fact = s↑-inc s j

s↑-inc-≤ : ∀ s i j → i N.≤ j → (s ↑) i ≤ (s ↑) j
s↑-inc-≤ s i j (0 , i≡j) = inr (cong (s ↑) (sym i≡j))
s↑-inc-≤ s i j (suc k , k+i+1≡j) = inl (s↑-inc' s i j (k , N.+-suc _ _ ∙ k+i+1≡j))

s↑-spec->ω : ∀ s i → s i ≡ tt → ω < (s ↑) (suc (suc i))
s↑-spec->ω s i si≡tt = goal
   where
    n : ℕ
    n = fst (least-index-true-spec-tt s i si≡tt)
    n≤i : n N.≤ i
    n≤i = fst (snd (least-index-true-spec-tt s i si≡tt))
    p : least-index-true s n ≡ tt
    p = snd (snd (least-index-true-spec-tt s i si≡tt))
    claim₀ : (s ↑) (suc n) ≡ ω
    claim₀ = cong (if_then ω else ((s ↑) n + 𝟏)) p
    n+1<i+2 : suc n N.< suc (suc i)
    n+1<i+2 = N.suc-≤-suc (N.suc-≤-suc n≤i)
    claim₁ : (s ↑) (suc n) < (s ↑) (suc (suc i))
    claim₁ = s↑-inc' s (suc n) (suc (suc i)) n+1<i+2
    goal : ω < (s ↑) (suc (suc i))
    goal = ≤∘<-in-< (inr claim₀) claim₁

s↑-bounded-by-ω+i : ∀ s i → (s ↑) i < ω + NtoC i
s↑-bounded-by-ω+i s 0 = <₁
s↑-bounded-by-ω+i s (suc i) = cases case₀ case₁
   where
    cases : {b : Bool} {A : Type}
          → (b ≡ tt → A) → (b ≡ ff → A) → A
    cases {ff} f g = g refl
    cases {tt} f g = f refl
    case₀ : least-index-true s i ≡ tt → (s ↑) (suc i) < ω + NtoC (suc i)
    case₀ p = ≤∘<-in-< (inr (sym claim₀)) claim₁
     where
      claim₀ : (s ↑) (suc i) ≡ ω
      claim₀ = cong (if_then ω else ((s ↑) i + 𝟏)) p
      claim₁ : ω < ω + NtoC (suc i)
      claim₁ = <₃ refl <₁
    case₁ : least-index-true s i ≡ ff → (s ↑) (suc i) < ω + NtoC (suc i)
    case₁ p = ≤∘<-in-< (inr (sym claim₀)) claim₁
     where
      claim₀ : (s ↑) (suc i) ≡ (s ↑) i + 𝟏
      claim₀ = cong (if_then ω else ((s ↑) i + 𝟏)) p
      IH : (s ↑) i < ω + NtoC i
      IH = s↑-bounded-by-ω+i s i
      lemma : ∀ i x → x < ω + NtoC i → x + 𝟏 < ω + NtoC (suc i)
      lemma 0 x p with x<ω-finite (x + 𝟏) (ω^-is-add-indecomposable x 𝟏 p (<₂ <₁))
      ... | (n , x+1=n) = subst (_< ω + 𝟏) (sym x+1=n) (<-trans (NtoC<ω n) (<₃ refl <₁))
      lemma (suc i) x p with <-tri x ω
      lemma (suc i) x p | inl x<ω = <-trans (ω^-is-add-indecomposable x 𝟏 x<ω (<₂ <₁)) (+r-is-<-monotone ω 𝟎 (NtoC (suc (suc i))) <₁)
      lemma (suc i) x p | inr x≥ω with x<ω+ω-finite x x≥ω (<-trans p (+r-is-<-monotone ω (NtoC (suc i)) ω (NtoC<ω (suc i))))
      lemma (suc i)x p | inr x≥ω | (n , x=ω+n) = subst (λ z → z + 𝟏 < ω + NtoC (suc (suc i))) (sym x=ω+n) (subst2 (_<_) (+-is-assoc ω (NtoC n) 𝟏) (cong (ω +_) (sym (NtoC⟨suc⟩≡1+NtoC (suc i)))) (+r-is-<-monotone ω (NtoC n + 𝟏) (𝟏 + NtoC (suc i)) (subst (_< _) (sym (NtoC⟨suc⟩≡1+NtoC n) ∙ sym (ω^𝟎+-is-+𝟏 (NtoC n) _)) (+r-is-<-monotone 𝟏 _ _ (+-left-cancellation-< ω (NtoC n) (NtoC (suc i)) (subst (_< (ω + NtoC (suc i))) x=ω+n p))))))
      claim₁ : (s ↑) i + 𝟏 < ω + NtoC (suc i)
      claim₁ = (lemma i ((s ↑) i) IH)

s↑-bounded-by-ω+ω : ∀ s i → (s ↑) i < ω + ω
s↑-bounded-by-ω+ω s i = <-trans (s↑-bounded-by-ω+i s i) (+r-is-<-monotone ω (NtoC i) ω (NtoC<ω i))

s↑-bounded-below-by-i : ∀ s i → (s ↑) (suc i) > NtoC i
s↑-bounded-below-by-i s i with least-index-true s i
s↑-bounded-below-by-i s ℕ.zero | ff = <₁
s↑-bounded-below-by-i s (suc i) | ff = subst (_< (s ↑) (suc i) + 𝟏) (sym (NtoC⟨suc⟩≡NtoC+𝟏 i)) (succ-is-<-monotone (s↑-bounded-below-by-i s i))
s↑-bounded-below-by-i s i | tt = NtoC<ω i


s↑-spec->ω' : ∀ s i n → s i ≡ tt → i N.< n → (s ↑) (suc n) ≥ ω + NtoC (n N.∸ i)
s↑-spec->ω' s i n si=tt i<n with least-index-true-spec-tt s i si=tt
s↑-spec->ω' s i n si=tt i<n | (j , (j≤i , lit=tt)) = (≤-trans (+r-is-≤-monotone ω (NtoC (n N.∸ i)) (NtoC (n N.∸ j)) (NtoC-is-≤-monotone (∸-lemma n i j j≤i))) (s↑-spec->ω'-lemma s j n lit=tt (N.≤<-trans j≤i i<n)))  where
  ∸-lemma : ∀ n i j → j N.≤ i → n N.∸ i N.≤ n N.∸ j
  ∸-lemma n i j (ℕ.zero , p) = subst (λ z → n N.∸ z N.≤ n N.∸ j) p N.≤-refl
  ∸-lemma n ℕ.zero j (suc k , p) = ⊥-rec (N.snotz p)
  ∸-lemma n (suc i) j (suc k , p) = N.≤-trans (lem n i) (∸-lemma n i j (k , (injSuc p)))
    where
      lem : ∀ n i → n N.∸ suc i N.≤ n N.∸ i
      lem ℕ.zero ℕ.zero = N.≤-refl
      lem ℕ.zero (suc i) = N.≤-refl
      lem (suc n) ℕ.zero = 1 , refl
      lem (suc n) (suc i) = lem n i
  s↑-spec->ω'-lemma : ∀ s i n → least-index-true s i ≡ tt → i N.< n → (s ↑) (suc n) ≥ ω + NtoC (n N.∸ i)
  s↑-spec->ω'-lemma s i n p i<n with least-index-true s n ≟ tt
  s↑-spec->ω'-lemma s i n p i<n | yes eq = ⊥-rec (true≢false (sym (least-index-true-is-true s i p) ∙ least-index-true-case-tt s n eq i i<n))
  s↑-spec->ω'-lemma s i ℕ.zero p i<n | no ¬eq = ⊥-rec (N.¬-<-zero i<n)
  s↑-spec->ω'-lemma s i (suc n) p (ℕ.zero , q) | no ¬eq = subst2 (λ z z' → z' ≤ (if z then ω else (s ↑) (suc n) + 𝟏)) (sym (¬true→false (least-index-true s (suc n)) ¬eq)) (sym (+-is-assoc ω (NtoC (n N.∸ i)) 𝟏) ∙ cong (ω +_) (lemma' (injSuc q))) (subst2 (λ z z' → z ≤ (if z' then ω else ((s ↑) n + 𝟏)) + 𝟏) (+-is-assoc ω (NtoC (n N.∸ i)) 𝟏) (sym p ∙ cong (least-index-true s) (injSuc q)) (inr (cong (ω +_) (sym (lemma'' (injSuc q))))))
    where
      lemma'' : ∀ {n} {i} → i ≡ n → NtoC (n N.∸ i) + 𝟏 ≡ 𝟏
      lemma'' {n} {i} i=n = cong (λ z → NtoC (z N.∸ i) + 𝟏) (sym i=n) ∙ cong (λ z → NtoC z + 𝟏) (N.n∸n i)
      lemma' : ∀ {n} {i} → i ≡ n → NtoC (n N.∸ i) + 𝟏 ≡ NtoC (suc n N.∸ i)
      lemma' {n} {i} i=n = subst (λ z → NtoC (n N.∸ z) + 𝟏 ≡ NtoC (suc n N.∸ z)) (sym i=n) (subst2 (λ z z' →  NtoC z + 𝟏 ≡ NtoC z') (sym (N.n∸n n)) (sym (N.+∸ 1 n)) refl)

  s↑-spec->ω'-lemma s i (suc n) p (suc k , q) | no ¬eq = subst2 (λ z z' → z' ≤ (if z then ω else (s ↑) (suc n) + 𝟏)) (sym (¬true→false (least-index-true s (suc n)) ¬eq)) (sym (+-is-assoc ω (NtoC (n N.∸ i)) 𝟏) ∙ cong (ω +_) (lemma q)) (succ-is-≤-monotone (s↑-spec->ω'-lemma s i n p (k , (injSuc q)))) where
   lemma : ∀ {n} {i} {k} → suc (k N.+ suc i) ≡ suc n → NtoC (n N.∸ i) + 𝟏 ≡ NtoC (suc n N.∸ i)
   lemma {n} {i} {k} q = sym (NtoC⟨suc⟩≡NtoC+𝟏 (n N.∸ i)) ∙ cong NtoC eq where
        eq = suc (n N.∸ i)
               ≡⟨ sym (cong (λ z → suc (z N.∸ i)) (injSuc q)) ⟩
             suc ((k N.+ suc i) N.∸ i)
               ≡⟨ cong (λ z → suc (z N.∸ i)) (N.+-suc k i) ⟩
             suc ((suc k N.+ i) N.∸ i)
               ≡⟨ cong suc (N.+∸ (suc k) i) ⟩
             suc (suc k)
               ≡⟨ sym (N.+∸ (suc (suc k)) i) ⟩
             suc (suc (k N.+ i)) N.∸ i
               ≡⟨ cong (λ z → suc z N.∸ i) (sym (N.+-suc k i)) ⟩
             (suc k N.+ suc i) N.∸ i
               ≡⟨ cong (λ z → z N.∸ i) q ⟩
             suc n N.∸ i
               ∎


s↑-spec->ω-back : ∀ s n → ω < (s ↑) (suc n) → Σ[ i ∈ ℕ ] (i N.≤ n) × (s i ≡ tt)
s↑-spec->ω-back s n ω<s↑n = let (k , s↑n=ω+k) = x<ω+ω-finite ((s ↑) (suc n)) (inl ω<s↑n) (s↑-bounded-by-ω+ω s (suc n)) in (n N.∸ k) , N.∸-≤ n k , (least-index-true-is-true s (n N.∸ k) (s↑n=ω+k→lit⟨n-k⟩=tt s n k s↑n=ω+k))
  where
    s↑n=ω→lit⟨n⟩=tt : ∀ s n → (s ↑) (suc n) ≡ ω → least-index-true s n ≡ tt
    s↑n=ω→lit⟨n⟩=tt s n p with least-index-true s n
    ... | tt = refl
    ... | ff = ⊥-rec (lim-is-not-suc {ω} ∣ (NtoC , NtoC↑) , ω-is-lim-of-NtoC ∣ (subst is-strong-suc p (_ , (succ-calc-strong-suc ((s ↑) n)))))

    s↑n=ω+k→lit⟨n-k⟩=tt : ∀ s n k → (s ↑) (suc n) ≡ ω + NtoC k → least-index-true s (n N.∸ k) ≡ tt
    s↑n=ω+k→lit⟨n-k⟩=tt s n ℕ.zero p = s↑n=ω→lit⟨n⟩=tt s n p
    s↑n=ω+k→lit⟨n-k⟩=tt s ℕ.zero (suc k) p with s 0
    ... | ff = ⊥-rec (<-irrefl (<-trans (subst (_< ω) p (fin<ω 𝟏 refl)) (<₃ refl <₁)))
    ... | tt = refl
    s↑n=ω+k→lit⟨n-k⟩=tt s (suc n) (suc k) p = s↑n=ω+k→lit⟨n-k⟩=tt s n k (step s n p)
      where
        step : ∀ s n → (s ↑) (suc (suc n)) ≡ ω + NtoC (suc k) → (s ↑) (suc n) ≡ ω + NtoC k
        step s n p with least-index-true s (suc n)
        step s n p | tt = ⊥-rec (lim-is-not-suc {ω} ∣ (NtoC , NtoC↑) , ω-is-lim-of-NtoC ∣
                                                    (subst is-strong-suc ((sym (+-is-assoc ω (NtoC k) 𝟏) ∙ cong (ω +_) (sym (NtoC⟨suc⟩≡NtoC+𝟏 k))) ∙ sym p)
                                                                         (ω + NtoC k , succ-calc-strong-suc (ω + NtoC k))))
        step s n p | ff with least-index-true s n
        step s n p | ff | tt = succ-injective (p ∙ cong (ω +_) (NtoC⟨suc⟩≡NtoC+𝟏 k) ∙ +-is-assoc ω (NtoC k) 𝟏)
        step s n p | ff | ff = succ-injective (p ∙ cong (ω +_) (NtoC⟨suc⟩≡NtoC+𝟏 k) ∙ +-is-assoc ω (NtoC k) 𝟏)

s↑-spec-≥ω : ∀ s i → s i ≡ tt → (s ↑) (suc i) ≥ ω
s↑-spec-≥ω s i si≡tt = subst ((s ↑) (suc i) ≥_) s↑j+1≡ω s↑j+1≤s↑i+1
 where
  j : ℕ
  j = fst (least-index-true-spec-tt s i si≡tt)
  j≤i : j N.≤ i
  j≤i = fst (snd (least-index-true-spec-tt s i si≡tt))
  p : least-index-true s j ≡ tt
  p = snd (snd (least-index-true-spec-tt s i si≡tt))
  s↑j+1≡ω : (s ↑) (suc j) ≡ ω
  s↑j+1≡ω = cong (if_then ω else ((s ↑) j + 𝟏)) p
  j+1≤i+1 : suc j N.≤ suc i
  j+1≤i+1 = N.suc-≤-suc j≤i
  s↑j+1≤s↑i+1 : (s ↑) (suc j) ≤ (s ↑) (suc i)
  s↑j+1≤s↑i+1 = s↑-inc-≤ s _ _ j+1≤i+1

s↑-spec-≥ω+n : ∀ s i → s i ≡ tt → ∀ n → (s ↑) (suc i N.+ n) ≥ ω + NtoC n
s↑-spec-≥ω+n s i si≡tt 0 = subst (_≥ ω) (sym (cong (s ↑) (N.+-zero (suc i)))) (s↑-spec-≥ω s i si≡tt)
s↑-spec-≥ω+n s i si≡tt (suc n) = goal
 where
  IH : (s ↑) (suc i N.+ n) ≥ ω + NtoC n
  IH = s↑-spec-≥ω+n s i si≡tt n
  claim₀ : (s ↑) (suc i N.+ n) < (s ↑) (suc (suc i N.+ n))
  claim₀ = s↑-inc s (suc i N.+ n)
  claim₁ : (s ↑) (suc (suc i N.+ n)) ≡ (s ↑) (suc i N.+ suc n)
  claim₁ = cong (s ↑) (sym (N.+-suc (suc i) n))
  claim₂ : (s ↑) (suc i N.+ suc n) > ω + NtoC n
  claim₂ = ≤∘<-in-< IH (subst ((s ↑) (suc i N.+ n) <_) claim₁ claim₀)
  claim₃ : (s ↑) (suc i N.+ suc n) ≥ ω + NtoC n + 𝟏
  claim₃ = <→s≤ claim₂
  claim₄ : ω + NtoC n + 𝟏 ≡ ω + (NtoC n + 𝟏)
  claim₄ = sym (+-is-assoc ω (NtoC n) 𝟏)
  claim₅ : ω + (NtoC n + 𝟏) ≡ ω + (NtoC (suc n))
  claim₅ = cong (ω +_) (sym (NtoC⟨suc⟩≡NtoC+𝟏 n))
  goal : (s ↑) (suc i N.+ suc n) ≥ ω + NtoC (suc n)
  goal = subst ((s ↑) (suc i N.+ suc n) ≥_) (claim₄ ∙ claim₅) claim₃

s↑-spec-<ω-back : ∀ s n → (∀ i → (s ↑) i ≤ ω + NtoC n) → ∀ i → s i ≡ ff
s↑-spec-<ω-back s n s↑≤ω+n i = ¬true→false (s i) ¬si≡tt
 where
  ¬si≡tt : ¬ (s i ≡ tt)
  ¬si≡tt si≡tt = <-irrefl (<∘≤-in-< claim₁ claim₂)
   where
    claim₀ : (s ↑) (suc i N.+ n) ≥ ω + NtoC n
    claim₀ = s↑-spec-≥ω+n s i si≡tt n
    claim₁ : (s ↑) (suc (suc i N.+ n)) > ω + NtoC n
    claim₁ = ≤∘<-in-< claim₀ (s↑-inc s (suc i N.+ n))
    claim₂ : (s ↑) (suc (suc i N.+ n)) ≤ ω + NtoC n
    claim₂ = s↑≤ω+n (suc (suc i N.+ n))


having-limits-implies-WLPO :
    ((f : ℕ → Cnf) (b : Cnf) → (∀ i → f i < b) → is-<-increasing f →
     Σ[ a ∈ Cnf ] a is-sup-of f)
  → WLPO
having-limits-implies-WLPO h s = goal
 where
  a : Cnf
  a = fst (h (s ↑) (ω + ω) (s↑-bounded-by-ω+ω s) (s↑-inc s))
  a-is-sup : a is-sup-of (s ↑)
  a-is-sup = snd (h (s ↑) (ω + ω) (s↑-bounded-by-ω+ω s) (s↑-inc s))

  case-ω<a : ∀ i → s i ≡ tt → ω < a
  case-ω<a i si≡tt = <∘≤-in-< (s↑-spec->ω s i si≡tt) (fst a-is-sup (suc (suc i)))
  case₀ : a ≡ ω → ∀ k → s k ≡ ff
  case₀ a≡ω k = ¬true→false (s k) (λ sk≡tt → <-irreflexive (sym a≡ω) (case-ω<a k sk≡tt))

  case-a≡ω : (∀ i → s i ≡ ff) → a ≡ ω
  case-a≡ω p = ≤-antisym a≤ω ω≤a
   where
    a≤ω : a ≤ ω
    a≤ω = snd a-is-sup ω λ i → inl (s↑-spec-<ω s i (λ k _ → p k))
    lemma : ∀ x → x < ω → Σ[ i ∈ ℕ ] x < (s ↑) i
    lemma 𝟎 <₁ = 1 , <∘≤-in-< <₁ (inr (cong (if_then ω else ((s ↑) 0 + 𝟏)) (p 0)))
    lemma x@(ω^ 𝟎 + b [ r ]) (<₂ u) = suc i , claim
     where
      IH : Σ[ i ∈ ℕ ] b < (s ↑) i
      IH = lemma b (<-trans (right< 𝟎 b r) (<₂ u))
      i : ℕ
      i = fst IH
      b<s↑i : b < (s ↑) i
      b<s↑i = snd IH
      claim₀ : least-index-true s i ≡ ff
      claim₀ = least-index-true-spec-ff s i (λ k _ → p k)
      claim₁ : (s ↑) (suc i) ≡ (s ↑) i + 𝟏
      claim₁ = cong (if_then ω else ((s ↑) i + 𝟏)) claim₀
      claim₂ : b + 𝟏 < (s ↑) i + 𝟏
      claim₂ = succ-is-<-monotone b<s↑i
      claim₃ : b + 𝟏 ≡ x
      claim₃ = ω^𝟎+-is-+𝟏 b r
      claim : x < (s ↑) (suc i)
      claim = ≤∘<-in-< (inr claim₃) (<∘≤-in-< claim₂ (inr claim₁))
    lemma (ω^ ω^ _ + _ [ _ ] + _ [ _ ]) (<₂ (<₂ ()))
    lemma (ω^ ω^ _ + _ [ _ ] + _ [ _ ]) (<₂ (<₃ _ ()))
    ¬a<ω : ¬ (a < ω)
    ¬a<ω a<ω = ≤→≯ (fst a-is-sup i) a<s↑i
     where
      i : ℕ
      i = fst (lemma a a<ω)
      a<s↑i : a < (s ↑) i
      a<s↑i = snd (lemma a a<ω)
    ω≤a : ω ≤ a
    ω≤a = ≮→≥ ¬a<ω
  case₁ : ¬ a ≡ ω → ¬ (∀ k → s k ≡ ff)
  case₁ ¬a≡ω p = ¬a≡ω (case-a≡ω p)

  goal : (∀ k → s k ≡ ff) ⊎ (¬ (∀ k → s k ≡ ff))
  goal = cases case₀ case₁
   where
    cases : {x y : Cnf} {A B : Type}
          → (x ≡ y → A) → (¬ x ≡ y → B) → A ⊎ B
    cases {x} {y} f g with Cnf-is-discrete x y
    ... | yes x≡y = inl (f x≡y)
    ... | no ¬x≡y = inr (g ¬x≡y)

MP→limits-unique : MP →
                   ∀ f {f↑ : is-<-increasing f} g {g↑ : is-<-increasing g} → {x y : Cnf} →
                   x ≤ y → x is-lim-of (f , f↑) → y is-lim-of (g , g↑) → f simulated-by g
MP→limits-unique mp f {f↑} g {g↑} {x} {y} x≤y xlimf ylimq i = ∣ map-snd (λ {n} → h-spec-tt n) (mp h λ p → <-irrefl (≤∘<-in-< (≤-trans x≤y (y≤fi p)) (fi<x p))) ∣
  where
    h : ℕ → Bool
    h k = Sum.rec (λ _ →  ff) (λ _ → tt) (<-tri (g k) (f i))
    h-spec-tt : ∀ k → h k ≡ tt → f i ≤ g k
    h-spec-tt k hk=tt with <-tri (g k) (f i)
    ... | inl _ = ⊥-rec (false≢true hk=tt)
    ... | inr fi≤gk  = fi≤gk
    h-spec-ff : ∀ k → h k ≡ ff → g k < f i
    h-spec-ff k hk=ff with <-tri (g k) (f i)
    ... | inl gk<fi = gk<fi
    ... | inr _ = ⊥-rec (true≢false hk=ff)
    ∀khk=ff : ¬ (Σ[ n ∈ ℕ ] (h n ≡ tt)) → (k : ℕ) → h k ≡ ff
    ∀khk=ff p k = Dec→Stable (h k ≟ ff) λ hk≠ff → p (k , ¬false→true (h k) hk≠ff)
    ∀kgk<fi : ¬ (Σ[ n ∈ ℕ ] (h n ≡ tt)) → (k : ℕ) → g k < f i
    ∀kgk<fi p k = h-spec-ff k (∀khk=ff p k)
    y≤fi : ¬ (Σ[ n ∈ ℕ ] (h n ≡ tt)) → y ≤ f i
    y≤fi p = snd ylimq (f i) λ k → <-in-≤ (∀kgk<fi p k)
    fi<x : ¬ (Σ[ n ∈ ℕ ] (h n ≡ tt)) → f i < x
    fi<x p = <∘≤-in-< (f↑ i) (fst xlimf (suc i))