Todd Waugh Ambridge, January 2024

# Sequences

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

open import MLTT.Spartan
open import Notation.Order
open import Naturals.Order
open import UF.DiscreteAndSeparated
open import NotionsOfDecidability.Complemented

module TWA.Thesis.Chapter2.Sequences where

repeat : {X : š“¤ Ģ‡ } ā†’ X ā†’ ā„• ā†’ X
repeat Ī± _ = Ī±

map : {X : š“¤ Ģ‡ } {Y : š“„ Ģ‡ }
    ā†’ (X ā†’ Y) ā†’ (ā„• ā†’ X) ā†’ (ā„• ā†’ Y)
map f Ī± n = f (Ī± n)

zipWith : {X : š“¤ Ģ‡ } {Y : š“„ Ģ‡ } {Z : š“¦ Ģ‡ }
        ā†’ (X ā†’ Y ā†’ Z) ā†’ (ā„• ā†’ X) ā†’ (ā„• ā†’ Y) ā†’ (ā„• ā†’ Z)
zipWith f Ī± Ī² n = f (Ī± n) (Ī² n)

head : {X : š“¤ Ģ‡ } ā†’ (ā„• ā†’ X) ā†’ X
head Ī± = Ī± 0

tail : {X : š“¤ Ģ‡ } ā†’ (ā„• ā†’ X) ā†’ (ā„• ā†’ X)
tail Ī± = Ī± āˆ˜ succ

_āˆ·_ : {T : ā„• ā†’ š“¤ Ģ‡ } ā†’ T 0 ā†’ Ī  (T āˆ˜ succ) ā†’ Ī  T
(h āˆ· Ī±) 0 = h
(h āˆ· Ī±) (succ n) = Ī± n

_āˆ¼āæ_ : {X : ā„• ā†’ š“¤ Ģ‡ } ā†’ Ī  X ā†’ Ī  X ā†’ ā„• ā†’ š“¤ Ģ‡
(Ī± āˆ¼āæ Ī²) n = (i : ā„•) ā†’ i < n ā†’ Ī± i ļ¼ Ī² i

āˆ¼āæ-sym : {X : ā„• ā†’ š“¤ Ģ‡ } (Ī± Ī² : Ī  X) (n : ā„•)
       ā†’ (Ī± āˆ¼āæ Ī²) n
       ā†’ (Ī² āˆ¼āæ Ī±) n
āˆ¼āæ-sym Ī± Ī² n f i i<n = f i i<n ā»Ā¹

bounded-decidable-Ī  : {X : ā„• ā†’ š“¤ Ģ‡ }
                    ā†’ is-complemented X
                    ā†’ (n : ā„•)
                    ā†’ is-decidable (Ī  i źž‰ ā„• , (i < n ā†’ X i))
bounded-decidable-Ī  d 0 = inl (Ī» _ ())
bounded-decidable-Ī  {š“¤} {X} d (succ n)
 = Cases (bounded-decidable-Ī  d n) Ī³ā‚ (inr āˆ˜ Ī³ā‚‚)
 where
  Ī³ā‚ : ((i : ā„•) ā†’ (i < n ā†’ X i))
     ā†’ is-decidable ((i : ā„•) ā†’ (i < succ n ā†’ X i))
  Ī³ā‚ f = Cases (d n) (inl āˆ˜ Ī³ā‚ā‚) (inr āˆ˜ Ī³ā‚ā‚‚)
   where
    Ī³ā‚ā‚ : X n ā†’ (i : ā„•) ā†’ i < succ n ā†’ X i
    Ī³ā‚ā‚ Xn i i<sn
     = Cases (<-split i n i<sn) (f i) (Ī» e ā†’ transport X (e ā»Ā¹) Xn)
    Ī³ā‚ā‚‚ : Ā¬ X n ā†’ Ā¬ ((i : ā„•) ā†’ i < succ n ā†’ X i)
    Ī³ā‚ā‚‚ g f = g (f n (<-succ n))
  Ī³ā‚‚ : Ā¬ ((i : ā„•) ā†’ i < n ā†’ X i) ā†’ Ā¬ ((i : ā„•) ā†’ i < succ n ā†’ X i)
  Ī³ā‚‚ g f = g (Ī» i i<n ā†’ f i (<-trans i n (succ n) i<n (<-succ n)))

bounded-decidable-Ī£ : {X : ā„• ā†’ š“¤ Ģ‡ } ā†’ is-complemented X
                    ā†’ (n : ā„•)
                    ā†’ is-decidable (Ī£ i źž‰ ā„• , ((i < n) Ɨ X i))
bounded-decidable-Ī£ d 0 = inr (Ī» (i , i<0 , _) ā†’ i<0)
bounded-decidable-Ī£ {š“¤} {X} d (succ n)
 = Cases (bounded-decidable-Ī£ d n)
    (Ī» (i , i<n , Xi)
     ā†’ inl (i , <-trans i n (succ n) i<n (<-succ n) , Xi))
    (Ī» Ā¬Ī£i<n ā†’ Cases (d n)
      (Ī» Xn ā†’ inl (n , <-succ n , Xn))
      (Ī» Ā¬Xn ā†’ inr (Ī» (i , i<sn , Xi) ā†’ Cases (<-split i n i<sn)
        (Ī» i<n ā†’ Ā¬Ī£i<n (i , i<n , Xi))
        (Ī» iļ¼n ā†’ Ā¬Xn (transport X iļ¼n Xi)))))

āˆ¼āæ-decidable
 : {X : ā„• ā†’ š“¤ Ģ‡ }
 ā†’ ((n : ā„•) ā†’ is-discrete (X n))
 ā†’ (Ī± Ī² : Ī  X) ā†’ (n : ā„•) ā†’ is-decidable ((Ī± āˆ¼āæ Ī²) n)
āˆ¼āæ-decidable ds Ī± Ī² = bounded-decidable-Ī  (Ī» n ā†’ ds n (Ī± n) (Ī² n))
\end{code}