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

------------------------------------------------
-- bisimilarity between ν w and ν (Layer w _) --
------------------------------------------------

-- this is done by showing that νextend w i₀ is a weakly terminal coalgebra for ⟦ Wi₀ ⟧,
-- from which we get that "νextend w i₀ Leaf" (equal to "ν w i₀") and "ν ⟦ Wi₀ ⟧ Leaf"
-- are bisimilar

open import prelude
open import InteractionSystems.properties
open import equality
open import Layering


module Layering.WTC  {I : Set}
                     (w : IS I)
                     (i₀ : I) where

open IS w renaming (Command to A ; Response to D ; next to n)
open IS (w #) renaming (Command to A# ; Response to D# ; next to n#)

W : IS (A# i₀)
W = [ LayeredTS w i₀ ] ⊥

open IS W renaming (Command to LA ; Response to LD ; next to Ln)

-- We want to show that X = λ α → νextend w i₀ α is a weakly terminal coalgebra for ⟦ W ⟧
C : Pow (A# i₀)
C = νextend w i₀

elim : C ⊂ ⟦ W ⟧ C
elim {α} T =
  (λ _ γ → fst (νElim (T γ))) ,
  λ _ ds → snd (νElim (T (fst ds))) (snd ds)


module _ (X : Pow (A# i₀))
         (hyp : X ⊂ ⟦ W ⟧ X) where

  private Y : Pow I
  Y i = Σ (A# i₀)     (λ α →
        Σ (D# i₀ α)   (λ γ →
        n# α γ ≡ i   ×
        X α           ))

  private incl : Y ⊂ ⟦ w ⟧ Y
  incl {i} (α , (γ , (refl , x))) =
    fst (hyp x) ⋆ γ ,
    λ d → (α ◂ (λ γ → fst (hyp x) ⋆ γ)) , ((γ , d) , (refl , (snd (hyp x) ⋆)))

  intro :  X ⊂ C
  intro {α} x = λ γ → νIntro Y incl {n# α γ} (α , (γ , (refl , x)))



-- computation rule
comp : (X : Pow (A# i₀)) → (c : X ⊂ ⟦ W ⟧ X) (α : A# i₀) (x : X α) →
       elim (intro X c x) ≡ functoriality W X C (intro X c) (c x)
comp X c α x = sigma-eq-intro refl refl


wtc : WTC ([ LayeredTS w i₀ ] ⊥) (νextend w i₀)
wtc = record { elim = elim ; intro = intro ; comp = comp }