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

---------------------------------------------------
-- elementary definitions on interaction systems --
---------------------------------------------------

open import dtt


module InteractionSystems where


-- functoriality / monotonicity
functoriality : {I : Set} (w : IS I) (X Y : Pow I) → X ⊂ Y → ⟦ w ⟧ X ⊂ ⟦ w ⟧ Y
functoriality w X Y incl (a , f) = a , (λ d → incl (f d))




-- Composition of interaction systems
_○_ : {I : Set} → (w₁ : IS I) → (w₂ : IS I) → IS I    -- ○ is \ciw
w₁ ○ w₂ =
  let open IS w₁ renaming (Command to A₁ ; Response to D₁ ; next to n₁) in
  let open IS w₂ renaming (Command to A₂ ; Response to D₂ ; next to n₂) in
   record { Command = λ i → Σ (A₁ i) (λ a₁ → Π (D₁ i a₁) (λ d₁ → A₂ (n₁ a₁ d₁)));
            Response = λ i x → let a₁ = fst x in Σ (D₁ i a₁) (λ d₁ → D₂ (n₁ a₁ d₁) (snd x d₁))  ;
            next = λ x d₁₂ → let a₁ = fst x in
                             let f = snd x in
                             let d₁ = fst d₁₂ in
                             let d₂ = snd d₁₂ in
                               n₂ (f d₁) d₂ }


-- Duality
_⊥ : {I : Set} → IS I → IS I  -- ⊥ is \bot
w ⊥ = let open IS w renaming (Command to A; Response to D; next to n) in
      record { Command = λ i → (a : A i) → D i a ;
               Response = λ i d → A i ;
               next = λ {i} d a → n a (d a) }


-------------------------------------------
-- Transition systems                    --
-- They amount to elements of I → Fam(I) --
-------------------------------------------
record TS (I : Set) : Set₁ where
  field
    Transition : I → Set
    next : {i : I} → (t : Transition i) → I

-- Demonic update for a transition system
[_] : {I : Set} → TS I → IS I
[ g ] = record { Command = λ i → One ;
                 Response = λ i _ → TS.Transition g i ;
                 next = λ _ t → TS.next g t }

-- Angelic update
⟨_⟩ : {I : Set} → TS I → IS I             -- ⟨ and ⟩ are \< and \>
⟨ g ⟩ = record { Command = λ i → TS.Transition g i ;
                 Response = λ i _ → One ;
                 next = λ t _ → TS.next g t }




--------------------------------
-- weakly terminal coalgebras --
--------------------------------

open import equality

record WTC {I : Set} (w : IS I) (C : Pow I) : Set₁ where
    field
      elim : C ⊂ ⟦ w ⟧ C
      intro : (X : Pow I) → (X ⊂ ⟦ w ⟧ X) → X ⊂ C
      comp : (X : Pow I) → (coalg : X ⊂ ⟦ w ⟧ X) → (i : I) → (x : X i) →
                   elim (intro X coalg x)
                   ≡
                   functoriality w X C (intro X coalg) (coalg x)