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

-----------------------------
-- Generic DTT definitions --
-----------------------------



module dtt where


record One : Set where
  constructor ⋆             -- ⋆ is \star (\st is actually enough for emacs/Agda)
{-data One : Set where
    ⋆ : One   -- ⋆ is \star (\st is actually enough for emacs/Agda)-}


-- Sigma types
open import Agda.Builtin.Sigma public    -- Σ is \Sigma


-- Pi type: just a synomym that sometimes looks nice with Σ
Π : (A : Set) (P : A → Set) → Set        -- Π is \Pi
Π A P = (x : A) → P x


-- cartesian product
infixr  _×_
_×_ : Set → Set → Set
A × B = Σ A (λ _ → B)





-- abbreviations
Pow : Set → Set₁
Pow X = X → Set

Rel : Set → Set → Set₁
Rel X Y = X → Y → Set

_⊂_ : {I : Set} → Pow I → Pow I → Set    -- ⊂ is \sub (or \subset)
_⊂_ {I} U V = {i : I} → U i → V i

_==_ : {I : Set} → Pow I → Pow I → Set    -- ⊂ is \sub (or \subset)
_==_ {I} U V = (U ⊂ V) × (V ⊂ U)

_≬_ : {I : Set} → Pow I → Pow I → Set    -- ≬ is \between
_≬_ {I} U V = Σ I λ i → (U i) × (V i)

-- reversing a relation
_~ : {X : Set} → {Y : Set} → Rel X Y → Rel Y X
(R ~) y x = R x y

-- composing relations
_•_ : {I₁ : Set} {I₂ : Set} {I₃ : Set} → Rel I₂ I₃ → Rel I₁ I₂ → Rel I₁ I₃  -- • is \bub
_•_  {I₁} {I₂} {I₃} R₁ R₂ i₁ i₃ = Σ I₂ (λ i₂ → R₁ i₂ i₃ × R₂ i₁ i₂)


--------------------------------------------
-- Interaction systems                    --
-- They amount to elements of I → Fam²(I) --
--------------------------------------------
record IS (I : Set) : Set₁ where
  field
    Command : I → Set
    Response : (i : I) → Command i → Set
    next : {i : I} → (c : Command i) → Response i c → I


-- extension of an interaction system
⟦_⟧ : {I : Set} → IS I → Pow I → Pow I     -- ⟦ is \[[ and ⟧ is \]]
⟦ w ⟧ U i = let open IS w renaming (Command to A ; Response to D ; next to n) in
            Σ (A i) (λ a → Π (D i a) (λ d → U (n a d)))


---------------------------
-- greatest fixed points --
---------------------------

open import Agda.Builtin.Coinduction renaming (∞ to Lazy ; ♯_ to Freeze ; ♭ to Unfreeze)

-- I cannot use the following to define greatest fixed points, as the termination
-- checker doesn't see the definition is productive...
--⟦_⟧ : {I : Set} → IS I → Pow I → Pow I
--⟦ w ⟧ U i = let open IS w renaming (Command to A ; Response to D ; next to n) in
--            Σ (A i) (λ a → Π (D i a) (λ d → Lazy (U (n a d))))
--ν w i = let open IS w renaming (Command to A ; Response to D ; next to n) in
--            Σ (A i) (λ a → Π (D i a) (λ d → Lazy (ν w (n a d))))

data ν {I : Set} (w : IS I) (i : I) : Set where     -- ν is \nu
  Root : (a : IS.Command w i) →
         ((d : IS.Response w i a) → Lazy (ν w (IS.next w a d)))
      → ν w i

νElim : {I : Set} → {w : IS I} → ν w ⊂ ⟦ w ⟧ (ν w)
νElim {I} {w} {i} (Root a l) = ( a , (λ x → Unfreeze (l x)) )

νIntro : {I : Set} → {w : IS I} → (X : Pow I) → (X ⊂ ⟦ w ⟧ X) → {i : I} → (x : X i) → ν w i
νIntro {I} {w} X coalg {i} x =
  let open IS w renaming (Command to A ; Response to D ;next to n) in
  let a : A i
      a = fst (coalg x) in
  let f : (d : D i a) → ν w (n a d)
      f d = νIntro X coalg {n a d} (snd (coalg x) d) in
  Root a (λ d → Freeze (f d))


{-
record ν {I : Set} (w : IS I) (i : I) : Set where     -- ν is \nu
  coinductive
  field
    Root : IS.Command w i
    Branch : (d : IS.Response w i Root) → ν w (IS.next w Root d)


νElim : {I : Set} → {w : IS I} → ν w ⊂ ⟦ w ⟧ (ν w)
νElim {I} {w} {i} T = ν.Root T , λ x → ν.Branch T x


-- WHY isn't the following accepted ?
νIntro : {I : Set} → {w : IS I} → (X : Pow I) → (X ⊂ ⟦ w ⟧ X) → {i : I} → (x : X i) → ν w i
ν.Root (νIntro X coalg x) = fst (coalg x)
ν.Branch (νIntro X coalg x) d = νIntro X coalg (snd (coalg x) d)

-}

{-
module STREAM (I : Set)
  where
  record Stream (i : I) : Set where
    coinductive
    field
      hd : I
      tl : Stream hd

  repeat : (i : I)  → Stream i
  Stream.hd (repeat i) = i
  Stream.tl (repeat i) = repeat {!!}
-}