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

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

    module Codata.Sized.M.Bisimilarity where

    open import Level using (_⊔_)
    open import Size using (Size; ∞)
    open import Codata.Sized.Thunk using (Thunk; Thunk^R; force)
    open import Codata.Sized.M using (M; inf)
    open import Data.Container.Core using (Container)
    open import Data.Container.Relation.Binary.Pointwise using (Pointwise; _,_)
    open import Data.Product.Base using (_,_)
    open import Function.Base using (_∋_)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.Structures using (IsEquivalence)
    open import Relation.Binary.Definitions
      using (Reflexive; Symmetric; Transitive)
    import Relation.Binary.PropositionalEquality.Core as ≡

    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 (≡.refl , λ where p .force → refl)

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

      trans : ∀ {i} → Transitive (Bisim C i)
      trans (inf (≡.refl , f)) (inf (≡.refl , g)) =
        inf (≡.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}
        }