By Martin Escardo, 2 September 2011.

Modified in December 2011 assuming function extensionality (which is
not used directly in this module, but instead in
GenericConvergentSequence).

We prove that the generic convergent sequence ℕ∞ is compact, or
searchable, which amounts to Theorem-3·6 of the paper

   https://www.cs.bham.ac.uk/~mhe/papers/omniscient-journal-revised.pdf
   http://www.cs.bham.ac.uk/~mhe/.talks/dagstuhl2011/omniscient.pdf

(Continuity axioms and the fan principle are not assumed.)

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan
open import UF.FunExt

module TypeTopology.GenericConvergentSequenceCompactness (fe : funext 𝓤₀ 𝓤₀) where

open import CoNaturals.Type
open import MLTT.Two-Properties
open import Notation.CanonicalMap
open import TypeTopology.CompactTypes
open import UF.DiscreteAndSeparated
open import UF.PropTrunc

\end{code}

We recall the main notions defined in the above imported modules:

\begin{code}

private
 module recall {X : 𝓤 ̇ } where

  recall₀ : is-compact∙ X ＝ (Π p ꞉ (X → 𝟚) , Σ x₀ ꞉ X , (p x₀ ＝ ₁ → Π x ꞉ X , p x ＝ ₁))
  recall₁ : is-compact  X ＝ (Π p ꞉ (X → 𝟚) , (Σ x ꞉ X , p x ＝ ₀) + (Π x ꞉ X , p x ＝ ₁))
  recall₂ : is-discrete X ＝ ((x y : X) → (x ＝ y) + (x ≠ y))

  recall₀ = by-definition
  recall₁ = by-definition
  recall₂ = by-definition

\end{code}

This is the main theorem proved in this module.

\begin{code}

ℕ∞-compact∙ : is-compact∙ ℕ∞
ℕ∞-compact∙ p = a , Lemma
 where
  α : ℕ → 𝟚
  α        = p (ι )
  α (succ n) = min𝟚 (α n) (p (ι (succ n)))

  d : is-decreasing α
  d n = Lemma[minab≤₂a] {α n}

  a : ℕ∞
  a = (α , d)

  Dagger₀ : (n : ℕ) → a ＝ ι n → p (ι n) ＝ ₀
  Dagger₀  r =  p (ι )   ＝⟨ refl ⟩
                 α        ＝⟨ ap (λ - → ι - ) r ⟩
                 ι (ι )  ＝⟨ refl ⟩
                 ₀         ∎
  Dagger₀ (succ n) r = p (ι (succ n))          ＝⟨ w ⁻¹ ⟩
                       α (succ n)              ＝⟨ ap (λ - → ι - (succ n)) r ⟩
                       ι (ι (succ n)) (succ n) ＝⟨ ℕ-to-ℕ∞-diagonal₀ n ⟩
                       ₀                       ∎
   where
    t = α n              ＝⟨ ap (λ - → ι - n) r  ⟩
        ι (ι (succ n)) n ＝⟨ ℕ-to-ℕ∞-diagonal₁ n ⟩
        ₁                ∎

    w = α (succ n)              ＝⟨ ap (λ - → min𝟚 - (p (ι (succ n)))) t ⟩
        min𝟚 ₁ (p (ι (succ n))) ＝⟨ refl ⟩
        p (ι (succ n))          ∎

  Dagger₁ : a ＝ ∞ → (n : ℕ) → p (ι n) ＝ ₁
  Dagger₁ r  = p (ι ) ＝⟨ refl ⟩
                α      ＝⟨ ap (λ - → ι - ) r ⟩
                ι ∞    ＝⟨ refl ⟩
                ₁       ∎
  Dagger₁ r (succ n) = p (ι (succ n)) ＝⟨ w ⁻¹ ⟩
                       α (succ n)     ＝⟨ ap (λ - → ι - (succ n)) r ⟩
                       ι ∞ (succ n)   ＝⟨ refl ⟩
                       ₁              ∎
   where
    s : α n ＝ ₁
    s = ap (λ - → ι - n) r

    w = α (succ n)              ＝⟨ ap (λ - → min𝟚 - (p (ι (succ n)))) s ⟩
        min𝟚 ₁ (p (ι (succ n))) ＝⟨ refl ⟩
        p (ι (succ n))          ∎

  Lemma₀ : (n : ℕ) → a ＝ ι n → p a ＝ ₀
  Lemma₀ n t = p a     ＝⟨ ap p t ⟩
               p (ι n) ＝⟨ Dagger₀ n t ⟩
               ₀       ∎

  Claim₀ : p a ＝ ₁ → (n : ℕ) → a ≠ ι n
  Claim₀ r n s = equal-₁-different-from-₀ r (Lemma₀ n s)

  Claim₁ : p a ＝ ₁ → a ＝ ∞
  Claim₁ r = not-finite-is-∞ fe (Claim₀ r)

  Claim₂ : p a ＝ ₁ → (n : ℕ) → p (ι n) ＝ ₁
  Claim₂ r = Dagger₁ (Claim₁ r)

  Claim₃ : p a ＝ ₁ → p ∞ ＝ ₁
  Claim₃ r = p ∞ ＝⟨ (ap p (Claim₁ r))⁻¹ ⟩
             p a ＝⟨ r ⟩
             ₁   ∎

  Lemma : p a ＝ ₁ → (v : ℕ∞) → p v ＝ ₁
  Lemma r = ℕ∞-𝟚-density fe (Claim₂ r) (Claim₃ r)

\end{code}

Corollaries:

\begin{code}

ℕ∞-compact : is-compact ℕ∞
ℕ∞-compact = compact∙-types-are-compact ℕ∞-compact∙

ℕ∞-Compact : is-Compact ℕ∞ {𝓤}
ℕ∞-Compact = compact-types-are-Compact ℕ∞-compact

ℕ∞-Π-Compact : is-Π-Compact ℕ∞ {𝓤}
ℕ∞-Π-Compact = Σ-Compact-types-are-Π-Compact ℕ∞ ℕ∞-Compact

ℕ∞-Compact∙ : is-Compact∙ ℕ∞ {𝓤}
ℕ∞-Compact∙ = Compact-pointed-gives-Compact∙ ℕ∞-Compact ∞

ℕ∞→ℕ-is-discrete : is-discrete (ℕ∞ → ℕ)
ℕ∞→ℕ-is-discrete = discrete-to-power-compact-is-discrete fe ℕ∞-compact (λ u → ℕ-is-discrete)

ℕ∞→𝟚-is-discrete : is-discrete (ℕ∞ → 𝟚)
ℕ∞→𝟚-is-discrete = discrete-to-power-compact-is-discrete fe ℕ∞-compact (λ u → 𝟚-is-discrete)

module _ (fe' : FunExt) (pt : propositional-truncations-exist) where

 open import TypeTopology.WeaklyCompactTypes fe' pt

 ℕ∞-is-∃-compact : is-∃-compact ℕ∞
 ℕ∞-is-∃-compact = compact-types-are-∃-compact ℕ∞-compact

 ℕ∞-is-Π-compact : is-Π-compact ℕ∞
 ℕ∞-is-Π-compact = ∃-compact-types-are-Π-compact ℕ∞-is-∃-compact

\end{code}