Todd Waugh Ambridge, January 2024

# Interval object finite approximations

\begin{code}
{-# OPTIONS --without-K --safe #-}

open import MLTT.Spartan
open import UF.FunExt
open import Naturals.Addition renaming (_+_ to _+β„•_)
open import UF.Base
open import MLTT.SpartanList hiding (_∷_;⟨_⟩;[_])

open import TWA.Thesis.Chapter2.Vectors
open import TWA.Thesis.Chapter2.Sequences
open import TWA.Thesis.Chapter5.IntervalObject

module TWA.Thesis.Chapter5.IntervalObjectApproximation
 (fe : FunExt)
 (io : Interval-object fe 𝓀)
 where

open basic-interval-object-development fe io hiding (βˆ’1 ; O ; +1)

first-_ : {A : π“₯ Μ‡ } (n : β„•) β†’ (β„• β†’ A) β†’ Vec A n
first- n = Seq-to-Vec n

append-one : {X : π“₯ Μ‡ } {n : β„•} β†’ X β†’ Vec X n β†’ Vec X (succ n)
append-one {π“₯} {X} {0} y ⟨⟩ = y :: ⟨⟩
append-one {π“₯} {X} {succ n} y (x :: xs) = x :: append-one y xs

m : {n : β„•} β†’ Vec 𝕀 (succ n) β†’ 𝕀
m {0} (x :: ⟨⟩) = x
m {succ n} (x :: xs) = x βŠ• m xs

n-approx : (x y : β„• β†’ 𝕀) (n : β„•) β†’ 𝓀  Μ‡
n-approx x y n = Ξ£ (z , w) κž‰ 𝕀 Γ— 𝕀
               , m (append-one z ((first- n) x))
               ＝ m (append-one w ((first- n) y))

approximation : 𝓀  Μ‡
approximation = (x y : β„• β†’ 𝕀) β†’ Ξ  (n-approx x y) β†’ M x ＝ M y

multi-canc : (w z : 𝕀) (y : β„• β†’ 𝕀) (n : β„•)
           β†’ m (append-one w ((first- n) y))
           ＝ m (append-one z ((first- n) y))
           β†’ w ＝ z
multi-canc w .w y 0 refl = refl
multi-canc w z y (succ n) e
 = multi-canc w z (y ∘ succ) n
     (βŠ•-canc _ _ _ (βŠ•-comm _ _ βˆ™ e βˆ™ βŠ•-comm _ _))

one-sided-approx : (x : 𝕀) (y : β„• β†’ 𝕀)
                 β†’ ((n : β„•)
                    β†’ Ξ£ w κž‰ 𝕀 , x ＝ m (append-one w ((first- n) y)))
                 β†’ x ＝ M y
one-sided-approx x y f = M-propβ‚‚ ws y Ξ³ where
  ws : β„• β†’ 𝕀
  ws 0 = x
  ws (succ i) = pr₁ (f (succ i))
  Ξ³ : (i : β„•) β†’ ws i ＝ (y i βŠ• ws (succ i))
  Ξ³ 0 = prβ‚‚ (f 1)
  Ξ³ (succ i) = multi-canc
                 (ws (succ i))
                 (y (succ i) βŠ• ws (succ (succ i)))
                 y
                 (succ i) (prβ‚‚ (f (succ i)) ⁻¹
             βˆ™ (prβ‚‚ (f (succ (succ i)))
             βˆ™ Ξ΄'' y (ws (succ (succ i))) i))
   where
    Ξ΄'' : (y : β„• β†’ 𝕀) (z : 𝕀) (i : β„•)
        β†’ m (append-one z ((first- (succ (succ i))) y))
        ＝ m (append-one (y (succ i) βŠ• z) ((first- (succ i)) y))
    Ξ΄'' y z 0 = refl
    Ξ΄'' y z (succ i) = ap (y 0 βŠ•_) (Ξ΄'' (y ∘ succ) z i)

_++'_ : {n : β„•} {X : 𝓀 Μ‡ } β†’ Vec X n β†’ (β„• β†’ X) β†’ (β„• β†’ X)
_++'_ {n} {X} v Ξ± = Vec-to-Seq n Ξ± v

m-prop₁ : (n : β„•) (a b c : β„• β†’ 𝕀) (e : 𝕀)
        β†’ (m (append-one e ((first- succ n) a))
          βŠ• M ((first- n) b ++' Ξ» i β†’ (c (succ (i +β„• n)))))
        ＝ M ((append-one (a n βŠ• e) ((first- n) Ξ» i β†’ a i βŠ• b i))
            ++' (Ξ» i β†’ c (succ (i +β„• n))))
m-prop₁ 0 a b c e = M-prop₁ _ ⁻¹
m-prop₁ (succ n) a b c e
 = ap ((a 0 βŠ• (a 1 βŠ• m (append-one e ((first- n) (a ∘ succ ∘ succ))))) βŠ•_)
     (M-prop₁ ((first- succ n) b ++' (Ξ» i β†’ c (succ (i +β„• succ n)))))
     βˆ™ βŠ•-tran _ _ _ _
     βˆ™ ap ((a 0 βŠ• b 0) βŠ•_) (m-prop₁ n (tail a) (tail b) (tail c) e)
     βˆ™ M-prop₁ (append-one (a (succ n) βŠ• e)
         ((first- succ n) (Ξ» i β†’ a i βŠ• b i))
         ++' (Ξ» i β†’ c (succ (i +β„• succ n)))) ⁻¹

M-append-＝ : (x : β„• β†’ 𝕀) (n : β„•)
            β†’ M x
            ＝ M (append-one (x n) ((first- n) x)
                   ++' (Ξ» i β†’ x (succ (i +β„• n))))
M-append-＝ x 0 = M-prop₁ x
                   βˆ™ M-prop₁
                       (append-one (x 0) ((first- 0) x)
                         ++' (Ξ» i β†’ x (succ (i +β„• 0)))) ⁻¹
M-append-＝ x (succ n) = M-prop₁ x
                       βˆ™ ap (x 0 βŠ•_) (M-append-＝ (tail x) n)
                       βˆ™ M-prop₁
                           (append-one (x (succ n)) ((first- succ n) x)
                             ++' (Ξ» i β†’ x (succ (i +β„• succ n)))) ⁻¹

M-append-++-＝ : (x y : β„• β†’ 𝕀) (n : β„•)
     β†’ M (Ξ» i β†’ x i βŠ• y i)
     ＝ (m (append-one (y n) ((first- succ n) x))
         βŠ• M (((first- n) y) ++' (Ξ» i β†’ (x (succ (i +β„• n)))
                                      βŠ• (y (succ (i +β„• n))))))
M-append-++-＝ x y n = M-append-＝ (Ξ» i β†’ x i βŠ• y i) n
           βˆ™ m-prop₁ n x y (Ξ» i β†’ x i βŠ• y i) (y n) ⁻¹

append-++-= : (x y : β„• β†’ 𝕀) (w : 𝕀) (n : β„•)
        β†’ ((append-one w ((first- n) x)) ++' y)
        ＝ (((first- n) x) ++' (w ∷ y))
append-++-= x y w 0 = dfunext (fe 𝓀₀ 𝓀) (β„•-induction refl Ξ» _ _ β†’ refl)
append-++-= x y w (succ n) = dfunext (fe 𝓀₀ 𝓀) (β„•-induction refl
                           (Ξ» k _ β†’ happly (append-++-= (tail x) y w n) k))

tail-_ : {X : 𝓀 Μ‡ } β†’ β„• β†’ (β„• β†’ X) β†’ (β„• β†’ X)
(tail- 0) Ξ± = Ξ±
(tail- succ n) Ξ± = tail ((tail- n) Ξ±)

Mβ†’m : (Ξ± : β„• β†’ 𝕀) (n : β„•)
    β†’ M Ξ± ＝ m (append-one (M ((tail- n) Ξ±)) ((first- n) Ξ±))
M→m α 0 = refl
Mβ†’m Ξ± (succ n) = M-prop₁ Ξ±
               βˆ™ ap (Ξ± 0 βŠ•_)
               (transport
                    (Ξ» - β†’ M (tail Ξ±)
                         ＝ m (append-one (M -) ((first- n) (tail α))))
                    (γ α n) (M→m (tail α) n))
  where
    Ξ³ : (Ξ± : β„• β†’ 𝕀) (n : β„•) β†’ ((tail- n) (tail Ξ±)) ＝ ((tail- succ n) Ξ±)
    Ξ³ Ξ± 0 = refl
    Ξ³ Ξ± (succ n) = ap tail (Ξ³ Ξ± n)

tail-first' : {X : 𝓀 Μ‡ } {m : β„•}
            β†’ (a : Vec X (succ m)) (Ξ² : β„• β†’ X) (n : β„•)
            β†’ (tail- succ n) (a ++' Ξ²)
            ＝ (tail- n) (tl {𝓀} {m} {Ξ» _ β†’ X} a ++' Ξ²)
tail-first' {X} {m} (_ :: xs) Ξ² 0 = refl
tail-first' {X} {m} (_ :: xs) Ξ² (succ n)
 = ap tail (tail-first' {X} {m} (_ :: xs) Ξ² n)

tail-first : {X : 𝓀 Μ‡ }
           β†’ (Ξ± Ξ² : β„• β†’ X) (n : β„•)
           β†’ (tail- n) (((first- n) Ξ±) ++' Ξ²) ＝ Ξ²
tail-first Ξ± Ξ² 0 = refl
tail-first Ξ± Ξ² (succ n)
 = tail-first' ((first- (succ n)) Ξ±) Ξ² n βˆ™ tail-first (tail Ξ±) Ξ² n

first-first : {X : 𝓀 Μ‡ }
            β†’ (Ξ± Ξ² : β„• β†’ X) (n : β„•)
            β†’ ((first- n) ((first- n) Ξ± ++' Ξ²)) ＝ (first- n) Ξ±
first-first Ξ± Ξ² 0 = refl
first-first Ξ± Ξ² (succ n) = ap (Ξ± 0 ::_) (first-first (tail Ξ±) Ξ² n)

approx-holds : approximation
approx-holds x y f = βŠ•-canc (M x) (M y) (M (tail z)) Ξ³
 where
  z w : β„• β†’ 𝕀
  z n = pr₁ (pr₁ (f n))
  w n = prβ‚‚ (pr₁ (f n))
  w'' : (n : β„•) β†’ (β„• β†’ 𝕀)
  w'' n = (y n βŠ• w (succ n))
        ∷ (Ξ» i β†’ x (succ (i +β„• n))
          βŠ• z (succ (succ (i +β„• n))))
  Ξ³'' : (n : β„•) β†’ m (append-one (z n) ((first- n) x))
                ＝ m (append-one (w n) ((first- n) y))
  Ξ³'' n = prβ‚‚ (f n)
  Ξ³' : (n : β„•) β†’ Ξ£ w* κž‰ 𝕀 , M (Ξ» i β†’ x i βŠ• (tail z) i)
     ＝ m (append-one w* ((first- n) (Ξ» i β†’ y i βŠ• (tail z) i)))
  Ξ³' n = M (w'' n)
       , (M-append-++-＝ x (tail z) n
       βˆ™ ap (_βŠ• M ((first- n) (tail z) ++' (Ξ» i β†’ x (succ (i +β„• n))
                                           βŠ• tail z (succ (i +β„• n)))))
            (Ξ³'' (succ n))
       βˆ™ m-prop₁ n y (tail z) (Ξ» i β†’ x i βŠ• (tail z) i) (w (succ n))
       βˆ™ ap M (append-++-= (Ξ» i β†’ y i βŠ• (tail z) i)
                (Ξ» i β†’ x (succ (i +β„• n)) βŠ• (tail z) (succ (i +β„• n)))
            (w'' n 0) n)
       βˆ™ Mβ†’m (((first- n) (Ξ» i β†’ y i βŠ• (tail z) i) ++' (w'' n))) n
       βˆ™ (ap (Ξ» - β†’ m (append-one (M -)
               ((first- n)
                 ((first- n)
                 (Ξ» i β†’ y i βŠ• (tail z) i) ++' (w'' n)))))
          (tail-first (Ξ» i β†’ y i βŠ• (tail z) i) (w'' n) n)
        βˆ™ ap (Ξ» - β†’ m (append-one (M (w'' n)) -))
           (first-first (Ξ» i β†’ y i βŠ• (tail z) i) (w'' n) n)))
  Ξ³ : (M x βŠ• M (z ∘ succ)) ＝ (M y βŠ• M (z ∘ succ))
  γ = M-hom x (z ∘ succ)
        βˆ™ one-sided-approx
            (M (Ξ» i β†’ x i βŠ• pr₁ (pr₁ (f (succ i)))))
            (Ξ» i β†’ y i βŠ• z (succ i))
            Ξ³'
        βˆ™ M-hom y (z ∘ succ) ⁻¹

n-approx' : (β„• β†’ 𝕀) β†’ (β„• β†’ 𝕀) β†’ β„• β†’ 𝓀  Μ‡
n-approx' x y n = Ξ£ (z , w) κž‰ 𝕀 Γ— 𝕀
                , m (append-one z ((first- (succ n)) x))
                ＝ m (append-one w ((first- (succ n)) y))

n-approx'β†’n-approx
 : (x y : β„• β†’ 𝕀) β†’ Ξ  (n-approx' x y) β†’ Ξ  (n-approx x y)
n-approx'β†’n-approx x y f 0 = (u , u) , refl
n-approx'β†’n-approx x y f (succ n) = f n

fg-n-approx' : {X : π“₯ Μ‡ } β†’ (f g : X β†’ β„• β†’ 𝕀) β†’ β„• β†’ 𝓀 βŠ” π“₯ Μ‡
fg-n-approx' f g n
 = (βˆ€ x β†’ n-approx' (f x) (g x) n)
 β†’ (βˆ€ x β†’ n-approx' (f x) (g x) (succ n))

fg-approx-holds : {X : π“₯ Μ‡ } (f g : X β†’ β„• β†’ 𝕀)
                β†’ Ξ  (fg-n-approx' f g)
                β†’ βˆ€ x β†’ M (f x) ＝ M (g x)
fg-approx-holds {_} {X} f g h x
 = approx-holds (f x) (g x) (n-approx'β†’n-approx (f x) (g x) (Ξ³ x))
 where
  Ξ³ : (x : X) β†’ Ξ  (n-approx' (f x) (g x))
  Ξ³ x 0 = (g x 0 , f x 0) , βŠ•-comm _ _
  Ξ³ x (succ n) = h n (Ξ» y β†’ Ξ³ y n) x

cancellation-holds : cancellative fe _βŠ•_
cancellation-holds a b c f = M-idem a ⁻¹ βˆ™ Ξ³ βˆ™ M-idem b
 where
  n-approx-c : (i : β„•)
             β†’ m (append-one c ((first- i) (Ξ» _ β†’ a)))
             ＝ m (append-one c ((first- i) (Ξ» _ β†’ b)))
  n-approx-c 0 = refl
  n-approx-c 1 = f
  n-approx-c (succ (succ i))
   = (   a    βŠ• (a βŠ• wa)) ＝⟨ ap (_βŠ• (a βŠ• wa)) (βŠ•-idem a ⁻¹) ⟩
     ((a βŠ• a) βŠ• (a βŠ• wa)) ＝⟨ ap ((a βŠ• a) βŠ•_) (n-approx-c (succ i)) ⟩
     ((a βŠ• a) βŠ• (b βŠ• wb)) ＝⟨ βŠ•-tran a a b wb ⟩
     ((a βŠ• b) βŠ• (a βŠ• wb)) ＝⟨ ap (Ξ» - β†’ (a βŠ• b) βŠ• (a βŠ• -)) (IHβ‚‚ ⁻¹) ⟩
     ((a βŠ• b) βŠ• (a βŠ• wa)) ＝⟨ ap ((a βŠ• b) βŠ•_) (n-approx-c (succ i)) ⟩
     ((a βŠ• b) βŠ• (b βŠ• wb)) ＝⟨ ap (_βŠ• (b βŠ• wb)) (βŠ•-comm a b) ⟩
     ((b βŠ• a) βŠ• (b βŠ• wb)) ＝⟨ βŠ•-tran b a b wb ⟩
     ((b βŠ• b) βŠ• (a βŠ• wb)) ＝⟨ ap (Ξ» - β†’ (b βŠ• b) βŠ• (a βŠ• -)) (IHβ‚‚ ⁻¹) ⟩
     ((b βŠ• b) βŠ• (a βŠ• wa)) ＝⟨ ap ((b βŠ• b) βŠ•_) (n-approx-c (succ i)) ⟩
     ((b βŠ• b) βŠ• (b βŠ• wb)) ＝⟨ ap (_βŠ• (b βŠ• wb)) (βŠ•-idem b) ⟩
     (   b    βŠ• (b βŠ• wb)) ∎
   where
    wa = m (append-one c ((first- i) (Ξ» _ β†’ a)) )
    wb = m (append-one c ((first- i) (Ξ» _ β†’ b)))
    IHβ‚‚ : wa ＝ wb
    IHβ‚‚ = n-approx-c i
  Ξ³ : M (Ξ» _ β†’ a) ＝ M (Ξ» _ β†’ b)
  Ξ³ = approx-holds (Ξ» _ β†’ a) (Ξ» _ β†’ b) (Ξ» i β†’ (c , c) :: n-approx-c i)
\end{code}