Coalgebra.agda

module Coalgebra where

open import Coinduction
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat


data List (A : Set) : Set where
  ∅ˡ   : List A
  _∷ˡ_ : A → List A → List A

data Colist (A : Set) : Set where
  ∅   : Colist A
  _∷_ : A → ∞ (Colist A) → Colist A

even : {A : Set} → Colist A → Colist A
even ∅        = ∅
even (x ∷ xs) with ♭ xs
… | ∅          = x ∷ (♯ ∅)
… | (x' ∷ xs') = x ∷ (♯ (even (♭ xs')))

odd : {A : Set} → Colist A → Colist A
odd ∅        = ∅
odd (x ∷ xs) with ♭ xs
… | ∅          = ∅
… | (x' ∷ xs') = x' ∷ (♯ (odd (♭ xs')))

tail : {A : Set} → Colist A → Colist A
tail ∅        = ∅
tail (x ∷ xs) = ♭ xs

odd' : {A : Set} → even {A} ≡ odd ∘ tail
odd' = {!!}

merge : {A : Set} → Colist A → Colist A → Colist A
merge ∅ ys        = ys
merge (x ∷ xs) ys = x ∷ (♯ (merge ys (♭ xs)))

map : {A B : Set} → (A → B) → Colist A → Colist B
map f ∅        = ∅
map f (x ∷ xs) = (f x) ∷ (♯ (map f (♭ xs)))

iterate : {A : Set} → (A → A) → A → Colist A
iterate f z = z ∷ (♯ (iterate f (f z)))

take : {A : Set} → ℕ → Colist A → List A
take zero xs          = ∅ˡ
take (suc n) ∅        = ∅ˡ
take (suc n) (x ∷ xs) = x ∷ˡ (take n (♭ xs))


module _ where

  n-ℕ's : ℕ → Colist ℕ
  n-ℕ's zero    = ∅
  n-ℕ's (suc n) = (suc n) ∷ (♯ (n-ℕ's n))

  ℕ's : Colist ℕ
  ℕ's = iterate suc 0