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

open import prelude
open import RTC
open import equality


module RTC.eval-epsilon {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*)

open import RTC.comonad
open import Simulations using (linear-evaluation)
open import RTC.WTC w fun-ext
open import Bisimulation



private eval : ν (w * ⊥) ⊂ ν (w ⊥)
eval T = linear-evaluation (w *) w (counit.epsilon w) refl T

private lave : ν (w * ⊥) ⊂ ν (w ⊥)
lave {i} T = νIntro (ν (w * ⊥)) elim T

private R : Pow (states (w ⊥))
R (i , (T₁ , T₂)) = Σ (ν (w * ⊥) i) (λ T → (T₁ ≡ eval T) × T₂ ≡ lave T)

private init : {i : I} (T : ν (w * ⊥) i) → R (i , ((eval T) , (lave T)))
init T = T , (refl , refl)

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

private coalg : R ⊂ Φ (w ⊥) R
coalg {(i , (T₁ , T₂))} (T , (refl , refl)) =
      let d₁ : (a₁ : A i) → D i a₁
          d₁ = fst (νElim T₁) in
      let d₂ : (a₂ : A i) → D i a₂
          d₂ = fst (νElim T₂) in
      let d : (a* : A* i) → D* i a*
          d = fst (νElim T) in
      refl , (λ (a : A i) →
      let newT₁ : ν (w ⊥) (n a (d₁ a))
          newT₁ = snd (νElim T₁) a in
      let newT₂ : ν (w ⊥) (n a (d₂ a))
          newT₂ = snd (νElim T₂) a in
      let newT : ν (w * ⊥) (n* (single-a a) (d (single-a a)))
          newT = snd (νElim T) (single-a a) in

      (newT , (refl , refl)))


lemma : {i : I} (T : ν (w * ⊥) i) →
        linear-evaluation (w *) w (epsilon w) refl T
        ≈
        νIntro (ν (w * ⊥)) elim T
lemma {i} T = record { carrier = R ; coalg = coalg ; init = init T }