{-# OPTIONS --without-K --safe --guardedness --no-sized-types #-}

---------------------------------------------------
-- bisimulation between infinite data-structures --
---------------------------------------------------

open import prelude
open import equality


module Bisimulation where

module _ {I : Set} (w : IS I) where
  open IS w renaming (Command to A ; Response to D ; next to n)

  transport-d : {i : I} {a₁ a₂ : A i} → (a₁ ≡ a₂) → (D i a₁) → D i a₂
  transport-d {i} {a₁} {a₂} eq d = transport (D i) eq d

  transport-n : {i : I} {a₁ a₂ : A i} → (eq : a₁ ≡ a₂) → (d₁ : D i a₁) → n a₁ d₁ ≡ n a₂ (transport-d eq d₁)
  transport-n {i} {a₁} {a₂} eq d₁ = higher-transport (D i) (λ a d → n a₁ d₁ ≡ n a d) eq d₁ refl

  states : Set
  states = ν w ≬ ν w

  -- relation transformers: the trees have the same root, and every successor tree on
  -- the left is related to the corresponding successor on the right
  Φ : Pow states → Pow states
  Φ R ( i , ( T₁ , T₂ ) ) =
    let a₁ : A i
        a₁ = fst (νElim T₁)
        a₂ : A i
        a₂ = fst (νElim T₂) in
    Σ (a₁ ≡ a₂)       λ eq →
    Π (D i a₁)         λ d₁ →
      let next-T₁ : ν w (n a₁ d₁)
          next-T₁ = snd (νElim T₁) d₁ in
      let d₂ : D i a₂
          d₂ = transport-d eq d₁ in
      let next-T₂' : ν w (n a₂ d₂)
          next-T₂' = snd (νElim T₂) d₂ in
      let eqi : n a₁ d₁ ≡ n a₂ d₂
          eqi = transport-n eq d₁ in
      let next-T₂ : ν w (n a₁ d₁)
          next-T₂ = transport (ν w) (sym eqi) next-T₂' in
    R ( n a₁ d₁ , ( next-T₁ , next-T₂ ) )

  record Bisimilar {i : I} (T₁ T₂ : ν w i) : Set₁ where
    field
      carrier : Pow states
      coalg : carrier ⊂ Φ carrier
      init : carrier ( i , ( T₁ , T₂ ) )

_≈_ : {I : Set} {w : IS I} {i : I} (T₁ T₂ : ν w i) → Set₁      -- ≈ is \approx
_≈_ {I} {w} {i} T₁ T₂ = Bisimilar w T₁ T₂