open import Level hiding (zero ; suc)

module Chapter6.IDesc.FreeMonad 
         {ℓ k : Level}
         {I : Set k}
       where

open import Data.Unit
open import Data.Nat hiding (_*_)
open import Data.Fin hiding (lift)
open import Data.Vec
open import Data.Product

open import Chapter2.Logic

open import Chapter5.IDesc
open import Chapter5.IDesc.Tagged
open import Chapter5.IDesc.Fixpoint

--infix 40 _*_
infix  _*D_


_*D_ : tagDesc ℓ I → (I → Set ℓ) → tagDesc ℓ I
((cs , ds) , itags) *D X = (suc cs , (λ i → (`Σ (X i) λ _ → `1) ∷ 
                                            ds i)) ,
                           itags

_*_ : tagDesc ℓ I → (I → Set ℓ) → I → Set ℓ
D * X = μ (toDesc (D *D X))

`v : ∀{D X} → {i : I} → X i → (D * X) i
`v x = ⟨ lift zero , x , lift tt  ⟩

`comp : ∀{D X} → {i : I} → ⟦ toDesc D ⟧func (D * X) i → (D * X) i
`comp (lift k , xs) = ⟨ lift (suc k) , xs ⟩