Martin Escardo 2011.

\begin{code}

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

open import UF-FunExt

module Sequence (fe : βˆ€ 𝓀 π“₯ β†’ funext 𝓀 π“₯) where

open import SpartanMLTT hiding (_+_)
open import UF-Retracts
open import NaturalsAddition

_∢∢_ : {X : β„• β†’ 𝓀 Μ‡} β†’ X 0 β†’ ((n : β„•) β†’ X(succ n)) β†’ ((n : β„•) β†’ X n)
(x ∢∢ α) 0 = x
(x ∢∢ α) (succ n) = α n

head : {X : β„• β†’ 𝓀 Μ‡} β†’ ((n : β„•) β†’ X n) β†’ X 0
head Ξ± = Ξ± 0

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

head-tail-eta : {X : β„• β†’ 𝓀 Μ‡} {Ξ± : (n : β„•) β†’ X n} β†’ (head Ξ± ∢∢ tail Ξ±) ≑ Ξ±
head-tail-eta {𝓀} {X} = dfunext (fe 𝓀₀ 𝓀) lemma
 where
  lemma : {Ξ± : (n : β„•) β†’ X n} β†’ (i : β„•) β†’ (head Ξ± ∢∢ tail Ξ±) i ≑ Ξ± i
  lemma 0 = refl
  lemma (succ i) = refl

private cons : {X : β„• β†’ 𝓀 Μ‡} β†’ X 0 Γ— ((n : β„•) β†’ X(succ n)) β†’ ((n : β„•) β†’ X n)
cons(x , α) = x ∢∢ α

cons-retraction : {X : β„• β†’ 𝓀 Μ‡} β†’ retraction(cons {𝓀} {X})
cons-retraction Ξ± = (head Ξ± , tail Ξ±) , head-tail-eta

\end{code}

(In fact it is an equivalence, but I won't bother, until this is
needed.)

\begin{code}

itail : {X : β„• β†’ 𝓀 Μ‡} β†’ (n : β„•) β†’ ((i : β„•) β†’ X i) β†’ ((i : β„•) β†’ X(i + n))
itail n Ξ± i = Ξ±(i + n)

\end{code}

Added 16th July 2018. Corecursion on sequences β„• β†’ A.

                    p = (h,t)
             X ------------------> A Γ— X
             |                       |
             |                       |
          f  |                       | A Γ— f
             |                       |
             |                       |
             v                       v
         (β„• β†’ A) ---------------> A Γ— (β„• β†’ A)
                  P = (head, tail)


  head (f x) = h x
  tail (f x) = f(t x)

Or equivalentaily

  f x = cons (h x) (f (t x))

\begin{code}

module _ {𝓀 π“₯ : Universe}
         {A : 𝓀 Μ‡}
         {X : π“₯ Μ‡}
         (h : X β†’ A)
         (t : X β†’ X)
       where

 private f : X β†’ (β„• β†’ A)
 f x zero = h x
 f x (succ n) = f (t x) n

 seq-corec = f

 seq-corec-head : head ∘ f ∼ h
 seq-corec-head x = refl

 seq-corec-tail : tail ∘ f ∼ f ∘ t
 seq-corec-tail x = dfunext (fe 𝓀₀ 𝓀) (Ξ» n β†’ refl)

 seq-final : Ξ£! \(f : X β†’ (β„• β†’ A)) β†’ (head ∘ f ∼ h) Γ— (tail ∘ f ∼ f ∘ t)
 seq-final = (seq-corec , seq-corec-head , seq-corec-tail) , c
  where
   c : (f f' : X β†’ β„• β†’ A) β†’
         (head ∘ f ∼ h) Γ— (tail ∘ f ∼ f ∘ t) β†’
         (head ∘ f' ∼ h) Γ— (tail ∘ f' ∼ f' ∘ t) β†’ f ≑ f'
   c f f' (a , b) (c , d) = dfunext (fe π“₯ 𝓀) (Ξ» x β†’ dfunext (fe 𝓀₀ 𝓀) (r x))
    where
     r : (x : X) (n : β„•) β†’ f x n ≑ f' x n
     r x zero = a x βˆ™ (c x)⁻¹
     r x (succ n) = f x (succ n) β‰‘βŸ¨ ap (Ξ» - β†’ - n) (b x) ⟩
                    f (t x) n    β‰‘βŸ¨ r (t x) n ⟩
                    f' (t x) n   β‰‘βŸ¨ ( ap (Ξ» - β†’ - n) (d x)) ⁻¹ ⟩
                    f' x (succ n) ∎

 \end{code}

Added 11th September 2018.

\begin{code}

seq-bisimulation : {A : 𝓀 Μ‡} β†’ ((β„• β†’ A) β†’ (β„• β†’ A) β†’ π“₯ Μ‡) β†’ 𝓀 βŠ” π“₯ Μ‡
seq-bisimulation {𝓀} {π“₯} {A} R = (Ξ± Ξ² : β„• β†’ A) β†’ R Ξ± Ξ²
                                                 β†’ (head Ξ± ≑ head Ξ²)
                                                 Γ— R (tail Ξ±) (tail Ξ²)

seq-coinduction : {A : 𝓀 Μ‡} (R : (β„• β†’ A) β†’ (β„• β†’ A) β†’ π“₯ Μ‡)
                β†’ seq-bisimulation R β†’ (Ξ± Ξ² : β„• β†’ A) β†’ R Ξ± Ξ² β†’ Ξ± ≑ Ξ²
seq-coinduction {𝓀} {π“₯} {A} R b Ξ± Ξ² r = dfunext (fe 𝓀₀ 𝓀) (h Ξ± Ξ² r)
 where
  h : (Ξ± Ξ² : β„• β†’ A) β†’ R Ξ± Ξ² β†’ Ξ± ∼ Ξ²
  h Ξ± Ξ² r zero = pr₁ (b Ξ± Ξ² r)
  h Ξ± Ξ² r (succ n) = h (tail Ξ±) (tail Ξ²) (prβ‚‚ (b Ξ± Ξ² r)) n

\end{code}