```------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise equality of colists
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --guardedness #-}

module Codata.Musical.Colist.Bisimilarity where

open import Codata.Musical.Colist.Base
open import Codata.Musical.Notation
open import Level using (Level)
open import Relation.Binary.Core using (Rel; _=[_]⇒_)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Definitions
using (Reflexive; Symmetric; Transitive)

private
variable
a b : Level
A : Set a
B : Set b

-- xs ≈ ys means that xs and ys are equal.

infix 4 _≈_

data _≈_ {A : Set a} : Rel (Colist A) a where
[]  :                                       []     ≈ []
_∷_ : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ x ∷ ys

infixr 5 _∷_

-- The equality relation forms a setoid.

setoid : Set a → Setoid _ _
setoid A = record
{ Carrier       = Colist A
; _≈_           = _≈_
; isEquivalence = record
{ refl  = refl
; sym   = sym
; trans = trans
}
}
where
refl : Reflexive _≈_
refl {[]}     = []
refl {x ∷ xs} = x ∷ ♯ refl

sym : Symmetric _≈_
sym []        = []
sym (x ∷ xs≈) = x ∷ ♯ sym (♭ xs≈)

trans : Transitive _≈_
trans []        []         = []
trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)

module ≈-Reasoning where
import Relation.Binary.Reasoning.Setoid as EqR
private
open module R {a} {A : Set a} = EqR (setoid A) public

-- map preserves equality.

map-cong : (f : A → B) → _≈_ =[ map f ]⇒ _≈_
map-cong f []        = []
map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈)
```