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

----------------------------------------------------------
-- some elementary properties about interaction systems --
----------------------------------------------------------

open import prelude
open import equality

module InteractionSystems.properties where

module composition {I : Set} (w₁ w₂ : IS I) where

  -- Properties of composition
  lemma₁ : (X : Pow I) →
                      ⟦ w₁ ○ w₂ ⟧ X ⊂ ⟦ w₁ ⟧ (⟦ w₂ ⟧ X)
  lemma₁ X {i} f =
    ( (fst (fst f)) , (λ d₁ → ( (snd (fst f) d₁) , (λ d₂ → snd f ( d₁ , d₂ )))) )

  lemma₂ : (X : Pow I) →
                      ⟦ w₁ ⟧ (⟦ w₂ ⟧ X) ⊂ ⟦ w₁ ○ w₂ ⟧ X
  lemma₂ X {i} f =
    ( ( (fst f) , (λ d₁ → fst (snd f d₁)) ) , (λ d₁d₂ → snd (snd f (fst d₁d₂)) (snd d₁d₂)) )


  open import equality
  module _ (fun-ext : {X : Set} {Y : Pow X} (f g : (x : X) → Y x) (eq : (x : X) → (f x) ≡ (g x)) → f ≡ g) where

    lemma-eq₁ : {i : I} (X : Pow I) (p : ⟦ w₁ ⟧ (⟦ w₂ ⟧ X) i) → lemma₁ X (lemma₂ X p) ≡ p
    lemma-eq₁ {i} X (a , f) = sigma-eq-intro refl (fun-ext f _ λ d → refl)

    lemma-eq₂ : {i : I} (X : Pow I) (p : ⟦ w₁ ○  w₂ ⟧ X i) → lemma₂ X (lemma₁ X p) ≡ p
    lemma-eq₂ {i} X (a , f) = sigma-eq-intro refl (fun-ext f _ (λ d → refl))


-- Properties of duality

module duality {I : Set} (w : IS I) (X : Pow I)
               where

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

  lemma₁ : {i : I} → ⟦ w ⊥ ⟧ X i → Π (A i) λ a → Σ (D i a) (λ d → X (n a d))
  lemma₁ ( r , u ) a = ( r a , u a )

  lemma₂ : {i : I} → (Π (A i) λ a → Σ (D i a) (λ d → X (n a d))) → ⟦ w ⊥ ⟧ X i
  lemma₂ F = ( (λ a → fst (F a)) , (λ a → snd (F a)) )

  open import equality
  module _ (fun-ext : {X : Set} {Y : Pow X} (f g : (x : X) → Y x) (eq : (x : X) → (f x) ≡ (g x)) → f ≡ g) where


    lemma-eq₁ : {i : I} (F : Π (A i) λ a → Σ (D i a) (λ d → X (n a d))) → lemma₁ (lemma₂ F) ≡ F
    lemma-eq₁ {i} F = fun-ext (lemma₁ (lemma₂ F)) F
                      λ a → sigma-eq-intro refl refl

    lemma-eq₂ : {i : I} → (x : ⟦ w ⊥ ⟧ X i) → lemma₂ (lemma₁ x) ≡ x
    lemma-eq₂ (f , a) = sigma-eq-intro refl refl





module Updates {I : Set} ( v : TS I) (X : Pow I) where

  updateDualityLemma₁₁ : ⟦ [ v ] ⟧ X ⊂ ⟦ ⟨ v ⟩ ⊥ ⟧ X
  updateDualityLemma₁₁ {i} (⋆ , f) = (λ t → ⋆) , (λ t → f t)

  updateDualityLemma₁₂ : ⟦ ⟨ v ⟩ ⊥ ⟧ X ⊂ ⟦ [ v ] ⟧ X
  updateDualityLemma₁₂ {i} (t , f) = ⋆ , (λ t → f t)


  updateDualityLemma₂₁ : ⟦ ⟨ v ⟩ ⟧ X ⊂ ⟦ [ v ] ⊥ ⟧ X
  updateDualityLemma₂₁ {i} (t , f) = (λ _ → t) , f

  updateDualityLemma₂₂ : ⟦ [ v ] ⊥ ⟧ X ⊂ ⟦ ⟨ v ⟩ ⟧ X
  updateDualityLemma₂₂ {i} (t , f) = (t ⋆) , (λ _ → f ⋆)



  open import equality
  updateEquality₁₁ : {i : I} (p : ⟦ [ v ] ⟧ X i) → p ≡ updateDualityLemma₁₂ (updateDualityLemma₁₁ p)
  updateEquality₁₁ p = refl

  updateEquality₁₂ : {i : I} (p : ⟦ ⟨ v ⟩ ⊥ ⟧ X i) → p ≡ updateDualityLemma₁₁ (updateDualityLemma₁₂ p)
  updateEquality₁₂ p = refl


  updateEquality₂₁ : {i : I} (p : ⟦ ⟨ v ⟩ ⟧ X i) → p ≡ updateDualityLemma₂₂ (updateDualityLemma₂₁ p)
  updateEquality₂₁ p = refl

  updateEquality₂₂ : {i : I} (p : ⟦ [ v ] ⊥ ⟧ X i) → p ≡ updateDualityLemma₂₁ (updateDualityLemma₂₂ p)
  updateEquality₂₂ p = refl



-- the predicate ν ⟨ v ⟩ is a weakly terminal coalgebra for ⟦ ⟨ v ⟩ ⊥ ⊥ ⟧
module update-duality-WTC {I : Set} (v : TS I) where

  open import equality

  private C : Pow I
  C = ν ⟨ v ⟩

  private w : IS I
  w = ⟨ v ⟩ ⊥ ⊥

  elim : C ⊂ ⟦ w ⟧ C
  elim {i} T =
    (λ _ → fst (νElim T)) ,
    λ _ → snd (νElim T) ⋆

  intro : {X : Pow I} (hyp : X ⊂ ⟦ w ⟧ X) → X ⊂ C
  intro {X} hyp {i} x₀ = νIntro X (λ x → fst (hyp x) (λ _ → ⋆) , λ _ → snd (hyp x) λ _ → ⋆) x₀

  comp : (X : Pow I) → (c : X ⊂ ⟦ w ⟧ X) (i : I) (x : X i) →
         elim (intro c x) ≡ functoriality w X (ν ⟨ v ⟩) (intro c) (c x)
  comp X c i x = sigma-eq-intro refl refl



ν-WTC : {I : Set} (w : IS I) → WTC w (ν w)
ν-WTC w = record {
      elim = νElim ;
      intro = νIntro ;
      comp = λ X coalg i x → refl }