Alice Laroche, 4th of December 2024

We show that the type of conaturals defined by coinduction is
equivalent to the type of conaturals defined as generic convergent
sequences when assuming funext and that bisimilarity is equality.

\begin{code}

{-# OPTIONS --guardedness #-}

module Unsafe.CoNat-Equiv where

open import CoNaturals.Type
open import MLTT.Spartan
open import MLTT.Plus-Properties
open import MLTT.Two-Properties
open import UF.Equiv
open import UF.FunExt

\end{code}

This implementation of CoNat comes from the Cubical Agda Library.

\begin{code}

CoNat' : 𝓀₀ Μ‡
record CoNat : 𝓀₀ Μ‡

CoNat' = πŸ™ + CoNat
record CoNat where
 constructor conat
 coinductive
 field
  force : πŸ™ + CoNat

open CoNat public

pattern cozero = inl ⋆
pattern cosuc n = inr n

\end{code}

Because we can't reason about coinductive type equality in classical
Agda, we define an binary relation which is equivalent to equality.
The correctness of it is proven in the Cubical Agda Library.

Three types are needed in order to convince the termination checker
some functions terminates.

\begin{code}

record _＝C_ (x y : CoNat) : Set
data _＝C'_ (x y : CoNat') : Set
_＝C''_ : CoNat' β†’ CoNat' β†’ Set

cozero  ＝C'' cozero  = πŸ™
cozero  ＝C'' cosuc y = 𝟘
cosuc x ＝C'' cozero  = 𝟘
cosuc x ＝C'' cosuc y = x ＝C y

data _＝C'_  x y where
    con : x ＝C'' y β†’ x ＝C' y

record _＝C_ x y where
 coinductive
 field
  prove : force x ＝C' force y
open _＝C_

\end{code}

We can at least show that the relation is an equivalence relation.

\begin{code}

＝C-refl : βˆ€ {x y} β†’ x ＝ y β†’ x ＝C y
＝C'-refl : βˆ€ {x y} β†’ x ＝ y β†’ x ＝C' y

＝C-refl p .prove = ＝C'-refl (ap force p)
＝C'-refl {cozero} {cozero}   p = con ⋆
＝C'-refl {cosuc _} {cosuc _} p = con (＝C-refl (inr-lc p))

＝C-sym  : βˆ€ {x y} β†’ x ＝C y β†’ y ＝C x
＝C'-sym : βˆ€ {x y} β†’ x ＝C' y β†’ y ＝C' x

＝C-sym p .prove = ＝C'-sym (p .prove)
＝C'-sym {cozero}  {cozero}  (con p) = con ⋆
＝C'-sym {cosuc _} {cosuc _} (con p) = con (＝C-sym p)

＝C-trans : βˆ€ {x y z} β†’ x ＝C y β†’ y ＝C z β†’ x ＝C z
＝C'-trans : βˆ€ {x y z} β†’ x ＝C' y β†’ y ＝C' z β†’ x ＝C' z

＝C-trans p q .prove = ＝C'-trans (p .prove) (q .prove)
＝C'-trans {cozero} {cozero} {cozero}   (con p) (con q) = con ⋆
＝C'-trans {cosuc _} {cosuc _} {cosuc _} (con p) (con q) = con (＝C-trans p q)

\end{code}

We give a mapping from CoNat' to β„• β†’ 2 and use it to define a
criterion for the relationship defined above.

\begin{code}

CoNat'-to-β„•β†’πŸš : CoNat' β†’ (β„• β†’ 𝟚)
CoNat'-to-β„•β†’πŸš cozero  zero = β‚€
CoNat'-to-β„•β†’πŸš cozero (succ n) = β‚€
CoNat'-to-β„•β†’πŸš (cosuc x)  zero = ₁
CoNat'-to-β„•β†’πŸš (cosuc x) (succ n) = CoNat'-to-β„•β†’πŸš (x .force) n

CoNat-to-β„•β†’πŸš : CoNat β†’ (β„• β†’ 𝟚)
CoNat-to-β„•β†’πŸš x = CoNat'-to-β„•β†’πŸš (x .force)

CoNat-equality-criterion : (x y : CoNat)
                         β†’ ((n : β„•) β†’ CoNat-to-β„•β†’πŸš x n ＝ CoNat-to-β„•β†’πŸš y n)
                         β†’ x ＝C y
CoNat-equality-criterion' : (x y : CoNat')
                          β†’ ((n : β„•) β†’ CoNat'-to-β„•β†’πŸš x n ＝ CoNat'-to-β„•β†’πŸš y n)
                          β†’ x ＝C' y

CoNat-equality-criterion x y f .prove =
 CoNat-equality-criterion' (x .force) (y .force) f

CoNat-equality-criterion' cozero cozero       f =
 con ⋆
CoNat-equality-criterion' cozero (cosuc x)    f =
 con (zero-is-not-one (f 0))
CoNat-equality-criterion' (cosuc x) (cozero)  f =
 con (one-is-not-zero (f 0))
CoNat-equality-criterion' (cosuc x) (cosuc y) f =
 con (CoNat-equality-criterion x y (f ∘ succ))

\end{code}

Finally we write functions β„•βˆž β†’ CoNat and Conat β†’ β„•βˆž and show that
they give an equivalence between β„•βˆž and CoNat, assuming function
extensionality and that our equivalence relation is a bisimilarity
relation.

\begin{code}

f : β„•βˆž β†’ CoNat
f' : 𝟚 β†’ β„•βˆž β†’ CoNat'

f x .force = f' (β„•βˆž-to-β„•β†’πŸš x 0) x
f' β‚€ x = cozero
f' ₁ x = cosuc (f (Pred x))

is-decreasing-CoNat'-to-β„•β†’πŸš : βˆ€ x β†’ is-decreasing (CoNat'-to-β„•β†’πŸš x)
is-decreasing-CoNat'-to-β„•β†’πŸš (cozero)   zero    = ⋆
is-decreasing-CoNat'-to-β„•β†’πŸš (cozero)  (succ n) = ⋆
is-decreasing-CoNat'-to-β„•β†’πŸš (cosuc x)  zero    = ₁-top
is-decreasing-CoNat'-to-β„•β†’πŸš (cosuc x) (succ n) = is-decreasing-CoNat'-to-β„•β†’πŸš
                                                  (x .force)
                                                  n

is-decreasing-CoNat-to-β„•β†’πŸš : βˆ€ x β†’ is-decreasing (CoNat-to-β„•β†’πŸš x)
is-decreasing-CoNat-to-β„•β†’πŸš x n = is-decreasing-CoNat'-to-β„•β†’πŸš (x .force) n

g : CoNat β†’ β„•βˆž
g x = CoNat-to-β„•β†’πŸš x , is-decreasing-CoNat-to-β„•β†’πŸš x

CoNatβ‰ˆβ„•βˆž : funextβ‚€
         β†’ (bisim : βˆ€ x y β†’ x ＝C y β†’ x ＝ y)
         β†’ β„•βˆž ≃ CoNat
CoNatβ‰ˆβ„•βˆž fe bisim = f , (g , Ξ» - β†’ bisim _ _ (f∘g∼id -)) , (g , g∘f∼id)
 where
  g∘f∼id : g ∘ f ∼ id
  g∘f∼id x = β„•βˆž-to-β„•β†’πŸš-lc fe (dfunext fe (I x _ refl))
   where
    I : (x : β„•βˆž)
      β†’ (b : 𝟚) β†’ b ＝ β„•βˆž-to-β„•β†’πŸš x 0
      β†’ (n : β„•)
      β†’ β„•βˆž-to-β„•β†’πŸš (g (f x)) n ＝ β„•βˆž-to-β„•β†’πŸš x n
    I x β‚€ eq zero = ap (Ξ» - β†’ β„•βˆž-to-β„•β†’πŸš (g (conat (f' - x))) zero) eq ⁻¹ βˆ™ eq
    I x ₁ eq zero = ap (Ξ» - β†’ β„•βˆž-to-β„•β†’πŸš (g (conat (f' - x))) zero) eq ⁻¹ βˆ™ eq
    I x β‚€ eq (succ n) = ap (Ξ» - β†’ β„•βˆž-to-β„•β†’πŸš (g (conat (f' - x))) (succ n)) eq ⁻¹
                      βˆ™ ap (Ξ» - β†’ β„•βˆž-to-β„•β†’πŸš - (succ n))
                        ( is-Zero-equal-Zero fe {g (conat cozero)} refl
                        βˆ™ is-Zero-equal-Zero fe {x} (eq ⁻¹) ⁻¹)
    I x ₁ eq (succ n) = ap (Ξ» - β†’ β„•βˆž-to-β„•β†’πŸš (g (conat (f' - x))) (succ n)) eq ⁻¹
                      βˆ™ I (Pred x) _ refl n

  f∘g∼id : (x : CoNat) β†’ f (g x) ＝C x
  f∘g∼id x = CoNat-equality-criterion _ _ (I (x .force))
   where
    I : (x : CoNat')
      β†’ (n : β„•) β†’ CoNat-to-β„•β†’πŸš (f (g (conat x))) n ＝ CoNat-to-β„•β†’πŸš (conat x) n
    I (cozero) zero = refl
    I (cosuc Ξ±) zero = refl
    I (cozero) (succ n) = refl
    I (cosuc Ξ±) (succ n) = I (Ξ± .force) n

\end{code}