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

------------------------------------------------
-- bisimilarity between ν (w ⊥) and ν (w * ⊥) --
-- we show that ν (w * ⊥) is a weakly terminal coalgebra for w ⊥...

open import prelude
open import InteractionSystems.properties
open import equality
open import RTC
open import Simulations


module RTC.WTC
       {I : Set}
       (w : IS I)
       (fun-ext : {X : Set} {Y : Pow X} (f g : (x : X) → Y x) (eq : (x : X) → (f x) ≡ (g x)) → f ≡ g)
       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*)

private single-a : {i : I} (a : A i) → A* i
single-a a = a ◂ λ d → Leaf

private C : Pow I
C = ν (w * ⊥)

-- ν (w * ⊥) is a coalgebra for ⟦w ⊥⟧
elim : C ⊂ ⟦ w ⊥ ⟧ C
elim {i} T =
  let f : (a : A i) → D i a
      f a =  fst (fst (νElim T) (single-a a)) in
  f , λ (a : A i) → snd (νElim T) (single-a a)


-- ν (w * ⊥) is weakly terminal
module _ (X : Pow I)
         (hyp : X ⊂ ⟦ w ⊥ ⟧ X) where


  private f : {i : I} (x : X i) (a* : A* i) → D* i a*
  f x Leaf = ⋆
  f {i} x (a ◂ next) =
    let d : D i a
        d = fst (hyp x) a in
    d , f ((snd (hyp x) a)) (next d)

  private g : {i : I} (x : X i) (a* : A* i) → X (n* a* (f x a*))
  g x Leaf = x
  g x (a ◂ next) = g (snd (hyp x) a) (next (fst (hyp x) a))

  private incl :  X ⊂ ⟦ w * ⊥ ⟧ X
  incl {i} x =
    f x ,
    g x

  intro : X ⊂ C
  intro {i} x = νIntro X incl x


-- computation rule
comp : (X : Pow I) → (c : X ⊂ ⟦ w ⊥ ⟧ X) (i : I) (x : X i) →
       elim (intro X c x) ≡ functoriality (w ⊥) X C (intro X c) (c x)
comp X c i x =
  let T : Pow (A i)
      T a = ν (w * ⊥) (n a (fst (elim (intro X c x)) a)) in
  let f : (a : A i) → T a
      f a = snd (elim (intro X c x)) a in
  let g : (a : A i) → T a
      g a = snd (functoriality (w ⊥) X C (intro X c) (c x)) a in
  sigma-eq-intro refl (fun-ext f g (λ a → refl))


wtc : WTC (w ⊥) (ν (w * ⊥))
wtc = record { elim = elim ; intro = intro ; comp = comp }