{-# OPTIONS --guardedness #-}
open import Data.Nat renaming (ℕ to Nat)
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Data.List
open ≡-Reasoning

data Nat : Set where
  zero : () → Nat
  suc : Nat → Nat

zero + suc


codata CoNat : Set where
  zero : CoNat
  suc : CoNat → Nat

record Prod (A B : Set) : Set where
  field
    foo : A
    bar : B


snoc : ∀ {A : Set} → List A → A → List A
snoc [] x = x ∷ []
snoc (y ∷ ys) x = y ∷ snoc ys x

module _ (Sprite : Set) (blank : Sprite) where

  record Animation : Set where
    coinductive
    field
      sprite : Sprite
      advance : Animation
      
  open Animation
  
  loop : List Sprite → Animation
  sprite (loop []) = blank
  sprite (loop (s ∷ ss)) = s
  advance (loop []) = loop []
  advance (loop (s ∷ ss)) = loop (snoc ss s)

  dse : Animation → Animation
  sprite (dse a) = sprite a
  advance (dse a) = dse (advance (advance a))

  dso : Animation → Animation
  sprite (dso a) = sprite (advance a)
  advance (dso a) = dso (advance (advance a))


  record _≈_ (A B : Animation) : Set where
    coinductive
    field
      sprite-≡ : sprite A ≡ sprite B
      advance-≈ : advance A ≈ advance B

  lemma : ∀ {a : Animation} →
          advance (dse a) ≈ dso (advance a)

  lemma = {!!}