open import Level hiding (zero ; suc) open import Chapter5.IDesc open import Chapter5.IDesc.Tagged open import Chapter5.IDesc.Fixpoint open import Chapter5.IDesc.InitialAlgebra module Chapter6.IDesc.FreeMonad.Monad {ℓ k : Level} {I : Set k} (D : tagDesc ℓ I) where open import Function open import Data.Unit open import Data.Nat hiding (_*_ ; fold) open import Data.Fin hiding (fold ; lift) open import Data.Vec hiding (_>>=_) open import Data.Product open import Chapter2.Logic open import Chapter6.IDesc.FreeMonad open import Chapter6.IDesc.FreeMonad.IMonad apply : ∀{X Y} → (D : tagDesc ℓ I) → ({i : I} → X i → (D * Y) i) → {i : I} → ⟦ toDesc (D *D X) ⟧func (D * Y) i → (D * Y) i apply (cs , ds) σ (lift zero , xs , lift tt) = σ xs apply (cs , ds) σ (lift (suc k) , xs) = ⟨ lift (suc k) , xs ⟩ subst : ∀{X Y i} → (D * X) i → ({i : I} → X i → (D * Y) i) → (D * Y) i subst {X} dx σ = fold (toDesc (D *D X)) (apply D σ) dx monad : RawIMonad {I = I} (_*_ D) monad = record { return = `v {D = D} ; _>>=_ = subst }