    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The free monad construction on indexed containers
    ------------------------------------------------------------------------

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

    module Data.Container.Indexed.FreeMonad where

    open import Level using (Level; _⊔_; lower)
    open import Function.Base hiding (const)
    open import Effect.Monad.Predicate using (RawPMonad)
    open import Data.Container.Indexed using (Container; Command; Response; next; ⟦_⟧; μ)
    open import Data.Container.Indexed.Combinator hiding (id; _∘_)
    open import Data.Empty using (⊥; ⊥-elim)
    open import Data.Sum.Base using (inj₁; inj₂)
    open import Data.Product.Base using (_,_)
    open import Data.W.Indexed using (sup)
    open import Relation.Unary using (Pred; _⊆_; ⋃; _∈_; ｛_｝)
    open import Relation.Unary.PredicateTransformer using (Pt)
    open import Relation.Binary.PropositionalEquality.Core using (refl)

    ------------------------------------------------------------------------

    infixl 9 _⋆C_
    infix  9 _⋆_

    _⋆C_ : ∀ {i o c r} {I : Set i} {O : Set o} →
           Container I O c r → Pred O c → Container I O _ _
    C ⋆C X = const X ⊎′ C

    _⋆_ : ∀ {ℓ} {O : Set ℓ} → Container O O ℓ ℓ → Pt O ℓ
    C ⋆ X = μ (C ⋆C X)

    pattern returnP x = (inj₁ x , _)
    pattern doP c k   = (inj₂ c , k)

    inn : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} {X} →
          ⟦ C ⟧ (C ⋆ X) ⊆ C ⋆ X
    inn (c , k) = sup (doP c k)

    rawPMonad : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} →
                RawPMonad {ℓ = ℓ} (_⋆_ C)
    rawPMonad {C = C} = record
      { return? = return
      ; _=<?_  = _=<<_
      }
      where
      return : ∀ {X} → X ⊆ C ⋆ X
      return x = sup (inj₁ x , ⊥-elim ∘ lower)

      _=<<_ : ∀ {X Y} → X ⊆ C ⋆ Y → C ⋆ X ⊆ C ⋆ Y
      f =<< sup (returnP x) = f x
      f =<< sup (doP c k)   = inn (c , λ r → f =<< k r)

    leaf : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} {X : Pred O ℓ} →
           ⟦ C ⟧ X ⊆ C ⋆ X
    leaf (c , k) = inn (c , return? ∘ k)
      where
      open RawPMonad rawPMonad

    generic : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} {o}
              (c : Command C o) →
              o ∈ C ⋆ (⋃[ r ∶ Response C c ] ｛ next C c r ｝)
    generic c = inn (c , λ r → return? (r , refl))
      where
      open RawPMonad rawPMonad