    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Greatest fixpoint for indexed containers - using guardedness
    ------------------------------------------------------------------------

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

    module Data.Container.Indexed.Fixpoints.Guarded where

    open import Level using (Level; _⊔_)
    open import Codata.Musical.M.Indexed using (M)
    open import Data.Container.Indexed using (Container)
    open import Relation.Unary using (Pred)

    private
      variable
        o c r : Level
        O : Set o

    -- The least fixpoint can be found in `Data.Container`

    open Data.Container.Indexed public
      using (μ)

    -- This lives in its own module due to its use of guardedness.

    ν : Container O O c r → Pred O _
    ν = M