module ColistQuestion where

open import Data.Maybe
open import Data.Sum
open import Data.Product

record Colist (A : Set) : Set where
  constructor hd
  coinductive
  field
    Hd : Maybe (A × Colist A)
open Colist

iterate1 : ∀ {a} → (a → Maybe a) → a → Colist a
Hd (iterate1 {A} f a) = Just (a , loop (f a))
   where
     loop : Maybe A → Colist A
     loop Nothing   = hd Nothing
     loop (Just a') = iterate1 f a'