{-# OPTIONS --copatterns #-} open import Relation.Binary.PropositionalEquality record Stream A : Set where coinductive field head : A tail : Stream A open Stream map : ∀{A B} (f : A → B) (s : Stream A) → Stream B head (map f s) = f (head s) tail (map f s) = map f (tail s) iter : ∀ {A} (f : A → A) (a : A) → Stream A head (iter f a) = a tail (iter f a) = iter f (f a) record _~_ {A} (s t : Stream A) : Set where coinductive field ~head : head s ≡ head t ~tail : tail s ~ tail t open _~_ map-iter : ∀{A} (f : A → A) (a : A) → map f (iter f a) ~ iter f (f a) ~head (map-iter f a) = refl ~tail (map-iter f a) = map-iter f (f a)