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
  α :   𝟚
  α 0       = p (ι 0)
  α (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₀ 0 r =  p (ι 0)   =⟨ refl 
                 α 0       =⟨ ap  -  ι - 0) r 
                 ι (ι 0) 0 =⟨ 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 0 = p (ι 0) =⟨ refl 
                α 0     =⟨ ap  -  ι - 0) r 
                ι  0   =⟨ 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}