Martin Escardo, 11th September 2018
Completed by Todd Waugh Ambridge, 15th May 2020

We begin by defining a "closeness function"

  c : X → X → ℕ∞

such that

  c x y = ∞ ↔ x = y

for some examples of types X, including Baire, Cantor and ℕ∞.

That is, two points are equal iff they are infinitely close.  If we
have c x y = under n for n : ℕ, the intuition is that x and y can be
distinguished by a finite amount of information of size n.

(An application is to show that WLPO holds iff ℕ∞ is discrete.)

We then discuss further codistance axioms.

\begin{code}

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

open import MLTT.Spartan
open import UF.FunExt

module TWA.Closeness (fe : FunExt) where

open import CoNaturals.Arithmetic fe
open import CoNaturals.Type renaming (min to min')
open import CoNaturals.UniversalProperty fe
open import MLTT.Two-Properties
open import Naturals.Sequence fe
open import Notation.CanonicalMap
open import Notation.Order
open import UF.DiscreteAndSeparated

module sequences
        {𝓤 : Universe}
        (D : 𝓤 ̇ )
        (δ : is-discrete D)
       where

\end{code}

We denote the type of sequences over D by $, and define a closeness
function $ → $ → ℕ∞ using the fact that ℕ∞ is the final coalgebra of
the functor 𝟙 + (-), which we refer to as corecursion.

\begin{code}

 private
  𝓢 : 𝓤 ̇
  𝓢 =   D
  X : 𝓤 ̇
  X = 𝓢 × 𝓢
  f : (α β : 𝓢)  head α  head β  𝟙 {𝓤₀} + X
  f α β q = inr (tail α , tail β)
  g : (α β : 𝓢)  head α  head β  𝟙 {𝓤₀} + X
  g α β n = inl 
  p : X  𝟙 {𝓤₀} + X
  p (α , β) = cases (f α β) (g α β) (δ (head α) (head β))
  c : 𝓢  𝓢  ℕ∞
  c = curry (ℕ∞-corec p)

\end{code}

We use the private name "c" in this submodule, which is exported as
"closeness":

\begin{code}

 closeness : 𝓢  𝓢  ℕ∞
 closeness = c

\end{code}

The two defining properties of the function c are the following:

\begin{code}

 closeness-eq₀ : (α β : 𝓢)  head α  head β
                c α β  Zero
 closeness-eq₁ : (α β : 𝓢)  head α  head β
                c α β  Succ (c (tail α) (tail β))

 closeness-eq₀ α β n = γ r
  where
   t : δ (head α) (head β)  inr n
   t = discrete-inr (fe 𝓤 𝓤₀) δ (head α) (head β) n
   r : p (α , β)  inl 
   r = ap (cases (f α β) (g α β)) t
   γ : p (α , β)  inl   c α β  Zero
   γ = Coalg-morphism-Zero p (α , β) 

 closeness-eq₁ α β q = γ r
  where
   t : δ (head α) (head β)  inl q
   t = discrete-inl δ (head α) (head β) q
   r : p (α , β)  inr (tail α , tail β)
   r = ap (cases (f α β) (g α β)) t
   γ : p (α , β)  inr (tail α , tail β)
      c α β  Succ (c (tail α) (tail β))
   γ = Coalg-morphism-Succ p (α , β) (tail α , tail β)

\end{code}

That any sequence is infinitely close to itself is proved by
coinduction on ℕ∞ using closeness-eq₁:

\begin{code}

 infinitely-close-to-itself : (α : 𝓢)  c α α  
 infinitely-close-to-itself α = ℕ∞-coinduction R b (c α α)  γ
  where
   l :  α  c α α  Succ (c (tail α) (tail α))
   l α = closeness-eq₁ α α refl
   R : ℕ∞  ℕ∞  𝓤 ̇
   R u v = (Σ α  𝓢 , u  c α α) × (v  )
   b : ℕ∞-bisimulation R
   b .(c α α) . ((α , refl) , refl) = s , t , Pred-∞-is-∞
    where
     s : positivity (c α α)  positivity 
     s = ap positivity (l α)
     t : Σ α'  𝓢 , Pred (c α α)  c α' α'
     t = tail α , (ap Pred (l α)  Pred-Succ)
   γ : R (c α α) 
   γ = (α , refl) , refl

\end{code}

That any two infinitely close sequences are equal is proved by
coinduction on sequences, using both closeness-eq₀ (to rule out an
impossible case) and closeness-eq₁ (to establish the result):

\begin{code}

 infinitely-close-are-equal : (α β : 𝓢)  c α β    α  β
 infinitely-close-are-equal = seq-coinduction  α β  c α β  ) b
  where
   b : (α β : 𝓢)  c α β  
                  (head α  head β) × (c (tail α) (tail β)  )
   b α β q = d , e
    where
     l : head α  head β  c α β  Zero
     l = closeness-eq₀ α β
     d : head α  head β
     d = Cases (δ (head α) (head β))
           (p : head α  head β)
             p)
           (n : head α  head β)
             𝟘-elim (Zero-not-Succ (Zero    =⟨ (l n)⁻¹ 
                                     c α β   =⟨ q 
                                            =⟨ (Succ-∞-is-∞ (fe 𝓤₀ 𝓤₀))⁻¹ 
                                     Succ   )))
     e : c (tail α) (tail β)  
     e = ap Pred (Succ (c (tail α) (tail β)) =⟨ (closeness-eq₁ α β d)⁻¹ 
                  c α β                      =⟨ q 
                                            )

\end{code}

Symmetric property:

\begin{code}

 symmetric-property : (α β : 𝓢)  c α β  c β α
 symmetric-property α β = ℕ∞-coinduction R b (c α β) (c β α) γ
  where
   R : ℕ∞  ℕ∞  𝓤 ̇
   R u v = Σ \α  Σ \β  (u  c α β) × (v  c β α)
   b : ℕ∞-bisimulation R
   b .(c α β) .(c β α) (α , β , refl , refl)
     = s , t (δ (head α) (head β))
    where
     s : positivity (c α β)  positivity (c β α)
     s = Cases (δ (head α) (head β)) sₕ sₜ
      where
       sₕ : head α  head β  positivity (c α β)  positivity (c β α)
       sₕ p = successors-same-positivity
                (closeness-eq₁ α β p)
                (closeness-eq₁ β α (p ⁻¹))
       sₜ : head α  head β  positivity (c α β)  positivity (c β α)
       sₜ d = ap positivity
               (closeness-eq₀ α β d
                closeness-eq₀ β α  p  d (p ⁻¹)) ⁻¹)
     t : (head α  head β) + (head α  head β)
        R (Pred (c α β)) (Pred (c β α))
     t (inl p) = tail α , tail β
               , ap Pred (closeness-eq₁ α β p  Pred-Succ)
               , ap Pred (closeness-eq₁ β α (p ⁻¹)  Pred-Succ)
     t (inr d) = α , β
               , Pred-Zero-is-Zero' (c α β) (closeness-eq₀ α β d)
               , Pred-Zero-is-Zero' (c β α) (closeness-eq₀ β α  p  d (p ⁻¹)))
   γ : R (c α β) (c β α)
   γ = α , β , refl , refl

\end{code}

Ultra property:

\begin{code}

 closeness-eq₁' : (α β : 𝓢)  is-positive (c α β)
                 head α  head β
 closeness-eq₁' α β p = Cases (δ (head α) (head β)) id
    h≠  𝟘-elim (zero-is-not-one
    (is-Zero-Zero ⁻¹  ap  -  ι - 0) (closeness-eq₀ α β h≠ ⁻¹)  p)))

 open import Naturals.Order

 closeness-conceptually₁ : (α β : 𝓢) (n : )
                          ((k : )  k  n  α k  β k)
                          n  c α β
 closeness-conceptually₁ α β zero α≈ₙβ
  = transport (0 ⊏_) (closeness-eq₁ α β (α≈ₙβ 0 ) ⁻¹)
    (is-positive-Succ (c (tail α) (tail β)))
 closeness-conceptually₁ α β (succ n) α≈ₙβ
  = transport (succ n ⊏_) (closeness-eq₁ α β (α≈ₙβ 0 ) ⁻¹)
    (closeness-conceptually₁ (tail α) (tail β) n  m  α≈ₙβ (succ m)))

 closeness-conceptually₂ : (α β : 𝓢) (n : )
                          n  c α β
                          ((k : )  k  n  α k  β k)
 closeness-conceptually₂ α β n ⊏ₙcαβ zero k≤n
  = closeness-eq₁' α β (⊏-trans'' (c α β) n 0 k≤n ⊏ₙcαβ)
 closeness-conceptually₂ α β n ⊏ₙcαβ (succ k) k≤n
  = closeness-conceptually₂ (tail α) (tail β) k (transport (succ k ⊏_)
      (closeness-eq₁ α β (closeness-eq₁' α β (⊏-trans'' (c α β) n 0  ⊏ₙcαβ)))
      (⊏-trans'' (c α β) n (succ k) k≤n ⊏ₙcαβ))
    k (≤-refl k)

 min-split : (α β : ℕ∞) (n : )  n  uncurry min' (α , β)  n  α × n  β
 pr₁ (min-split α β n min≼) = different-from-₀-equal-₁
                               x  zero-is-not-one (Lemma[min𝟚ab=₀] (inl x) ⁻¹  min≼))
 pr₂ (min-split α β n min≼) = different-from-₀-equal-₁
                               x  zero-is-not-one (Lemma[min𝟚ab=₀] (inr x) ⁻¹  min≼))

 ultra-property : (α β ε : 𝓢)  min (c α β , c β ε)  c α ε
 ultra-property α β ε n min≼  = closeness-conceptually₁ α ε n
                      k k≤n  closeness-conceptually₂ α β n (pr₁ min-split') k k≤n
                               closeness-conceptually₂ β ε n (pr₂ min-split') k k≤n)
  where
   min-split' : n  c α β × n  c β ε
   min-split' = min-split (c α β) (c β ε) n
                (transport  -  n  - (c α β , c β ε)) min= min≼)

\end{code}

We now consider the following two special cases for the Baire and
Cantor types:

\begin{code}

open sequences  ℕ-is-discrete
 renaming
  (closeness                  to Baire-closeness ;
   infinitely-close-to-itself to Baire-infinitely-close-to-itself ;
   infinitely-close-are-equal to Baire-infinitely-close-are-equal ;
   symmetric-property         to Baire-symmetric-property ;
   ultra-property             to Baire-ultra-property )

open sequences 𝟚 𝟚-is-discrete
 renaming
  (closeness                  to Cantor-closeness ;
   infinitely-close-to-itself to Cantor-infinitely-close-to-itself ;
   infinitely-close-are-equal to Cantor-infinitely-close-are-equal ;
   symmetric-property         to Cantor-symmetric-property ;
   ultra-property             to Cantor-ultra-property )

\end{code}

And now we reduce the closeness of the Cantor type to the generic
convergent sequence:

\begin{code}

ℕ∞-closeness : ℕ∞  ℕ∞  ℕ∞
ℕ∞-closeness u v = Cantor-closeness (ι u) (ι v)

ℕ∞-infinitely-close-to-itself : (u : ℕ∞)  ℕ∞-closeness u u  
ℕ∞-infinitely-close-to-itself u = Cantor-infinitely-close-to-itself (ι u)

ℕ∞-equal-are-infinitely-close : (u v : ℕ∞)  u  v  ℕ∞-closeness u v  
ℕ∞-equal-are-infinitely-close u .u refl = ℕ∞-infinitely-close-to-itself u

ℕ∞-infinitely-close-are-equal : (u v : ℕ∞)  ℕ∞-closeness u v    u  v
ℕ∞-infinitely-close-are-equal u v r = ℕ∞-to-ℕ→𝟚-lc (fe 𝓤₀ 𝓤₀) γ
 where
  γ : ι u  ι v
  γ = Cantor-infinitely-close-are-equal (ι u) (ι v) r

ℕ∞-symmetric-property : (u v : ℕ∞)  ℕ∞-closeness u v  ℕ∞-closeness v u
ℕ∞-symmetric-property u v = Cantor-symmetric-property (ι u) (ι v)

ℕ∞-ultra-property : (u v w : ℕ∞)
                   min (ℕ∞-closeness u v , ℕ∞-closeness v w)  ℕ∞-closeness u w
ℕ∞-ultra-property u v w = Cantor-ultra-property (ι u) (ι v) (ι w)

\end{code}

Axioms for closeness:

\begin{code}

is-closeness
 indistinguishable-are-equal
 self-indistinguishable
 is-symmetric
 is-ultra
  : {X : 𝓤 ̇ }  (X  X  ℕ∞)  𝓤 ̇

indistinguishable-are-equal c =  x y  c x y    x  y
self-indistinguishable      c =  x  c x x  
is-symmetric                c =  x y  c x y  c y x
is-ultra                    c =  x y z  min (c x y , c y z)  c x z
is-closeness                c = indistinguishable-are-equal c
                              × self-indistinguishable c
                              × is-symmetric c
                              × is-ultra c

\end{code}

The above closenesss are indeed closenesss according
to this definition

\begin{code}

open sequences

ℕ→D-has-closeness : (X : 𝓤 ̇ ) (δ : is-discrete X)
                   is-closeness (closeness X δ)
ℕ→D-has-closeness X δ
 = infinitely-close-are-equal X δ
 , infinitely-close-to-itself X δ
 , symmetric-property X δ
 , ultra-property X δ

ℕ→ℕ-has-closeness : is-closeness (Baire-closeness)
ℕ→ℕ-has-closeness = ℕ→D-has-closeness  ℕ-is-discrete

ℕ→𝟚-has-closeness : is-closeness (Cantor-closeness)
ℕ→𝟚-has-closeness = ℕ→D-has-closeness 𝟚 𝟚-is-discrete

ℕ→ℕ∞-has-closeness : is-closeness (ℕ∞-closeness)
ℕ→ℕ∞-has-closeness = ℕ∞-infinitely-close-are-equal
                   , ℕ∞-infinitely-close-to-itself
                   , ℕ∞-symmetric-property
                   , ℕ∞-ultra-property