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 _*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 ⟩