{-# 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-bis  {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 =
  (λ (γ : D# i₀ α) → 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 = λ (γ : D# i₀ α) → νIntro Y incl {n# α γ} (α , (γ , (refl , x)))

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