------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed M-types (the dual of indexed W-types aka Petersson-Synek
-- trees).
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe --guardedness #-}

module Codata.Musical.M.Indexed where

open import Level
open import Codata.Musical.Notation
open import Data.Product.Base using (_,_; proj₁; proj₂)
open import Data.Container.Indexed.Core
open import Function.Base using (_∘_)
open import Relation.Unary

-- The family of indexed M-types.

module _ { c r} {O : Set } (C : Container O O c r) where

  data M (o : O) : Set (  c  r) where
    inf :  C  (  M) o  M o

  open Container C

  -- Projections.

  head : M  Command
  head (inf (c , _)) = c

  tail :  {o} (m : M o) (r : Response (head m))  M (next (head m) r)
  tail (inf (_ , k)) r =  (k r)

  force : M   C  M
  force (inf (c , k)) = c , λ r   (k r)

  -- Coiteration.

  coit :  {} {X : Pred O }  X   C  X  X  M
  coit ψ x = inf (proj₁ cs , λ r   coit ψ (proj₂ cs r))
    where
    cs = ψ x