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

-----------------------------
-- comonad structure of _* --
-----------------------------

open import dtt
open import equality
open import RTC
open import Simulations


module RTC.comonad where

module counit {I : Set}
              (w : IS I) where
  open IS w renaming (Command to A ; Response to D ; next to n)
  open RTC using (Leaf ; _◂_)
  open IS (w *) renaming (Command to A* ; Response to D* ; next to n*)

  private lemma : {i₁ : I} {i₂ : I} → (i₁ ≡ i₂) → Φ (w *) w _≡_ i₁ i₂
  lemma {i} refl a = (a ◂ (λ _ → Leaf)) , λ d → (fst d) , refl

  epsilon : (w *) ⊸ w
  epsilon = record { R = _≡_ ; coalg = lemma }

open counit using (epsilon) public


module comultiplication  {I : Set}
                         (w : IS I) where
  open IS w renaming (Command to A ; Response to D ; next to n)
  open RTC using (Leaf ; _◂_)
  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**)

  {-# TERMINATING #-}
  lemma : {i : I} → (a** : A** i) → ⟦ w * ⟧ (λ i' → Σ (D** i a**) λ d** → i' ≡ n** a** d**) i
  lemma {i} Leaf = Leaf , (λ _ → ⋆ , refl)
  lemma {i} (Leaf ◂ ass) =
              -- recursive call: we remove the root "Leaf" from the well-founded tree
              let rec-call = lemma (ass ⋆) in
              let a* : A* i
                  a* = fst rec-call in
              a*  , λ ds →
              (⋆ , fst (snd rec-call ds)) , snd (snd rec-call ds)
  lemma {i} ((a ◂ as) ◂ ass) =
              -- recursive call: we remove the root "a" from the well founded-tree
              let rec-call d = lemma ((as d) ◂ λ ds → ass (d , ds)) in
              let a* : A* i
                  a* = a ◂ λ d → fst (rec-call d) in
              a* , λ d* →
              let d : D i a
                  d = fst d* in
              let ni = n a d in
              let a** : A** ni
                  a** = as d ◂ λ ds → ass (d , ds) in
              let d** : D** ni a**
                  d** = fst (snd (rec-call d) (snd d*)) in
              let eq : n* a* d* ≡ n** a** d**
                  eq = snd (snd (rec-call d) (snd d*)) in
              ((d , fst d**) , snd d**) , eq

  private coalg : {i₁ i₂ : I} → i₁ ≡ i₂ →
                      Π (A** i₂) λ a** →
                      Σ (A* i₁) λ a* →
                      Π (D* i₁ a*) λ d* →
                      Σ (D** i₂ a**) λ d** →
                        n* a* d* ≡ n** a** d**
  coalg {i} refl a** = lemma a**

  delta : (w *) ⊸ (w * *)
  delta = record {
    R = _≡_ ;
    coalg = coalg
    }

open comultiplication using (delta) public