```------------------------------------------------------------------------
-- The Agda standard library
--
-- Bisimilarity for M-types
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --sized-types #-}

module Codata.Sized.M.Bisimilarity where

open import Level
open import Size
open import Codata.Sized.Thunk
open import Codata.Sized.M
open import Data.Container.Core
open import Data.Container.Relation.Binary.Pointwise using (Pointwise; _,_)
open import Data.Product using (_,_)
open import Function.Base using (_∋_)
open import Relation.Binary
import Relation.Binary.PropositionalEquality as P

data Bisim {s p} (C : Container s p) (i : Size) : Rel (M C ∞) (s ⊔ p) where
inf : ∀ {t u} → Pointwise C (Thunk^R (Bisim C) i) t u → Bisim C i (inf t) (inf u)

module _ {s p} {C : Container s p} where

-- unfortunately the proofs are a lot nicer if we do not use the combinators
-- C.refl, C.sym and C.trans

refl : ∀ {i} → Reflexive (Bisim C i)
refl {x = inf t} = inf (P.refl , λ where p .force → refl)

sym : ∀ {i} → Symmetric (Bisim C i)
sym  (inf (P.refl , f)) = inf (P.refl , λ where p .force → sym (f p .force))

trans : ∀ {i} → Transitive (Bisim C i)
trans (inf (P.refl , f)) (inf (P.refl , g)) =
inf (P.refl , λ where p .force → trans (f p .force) (g p .force))

isEquivalence : ∀ {i} → IsEquivalence (Bisim C i)
isEquivalence = record
{ refl  = refl
; sym   = sym
; trans = trans
}

setoid : {i : Size} → Setoid (s ⊔ p) (s ⊔ p)
setoid {i} = record
{ isEquivalence = isEquivalence {i}
}
```