------------------------------------------------------------------------
-- The Agda standard library
--
-- Sized fixpoints of containers, based on the work of Abbott and others
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --sized-types #-}

module Data.Container.Fixpoints.Sized where

open import Level using (Level; _⊔_)
open import Size using (Size)
open import Codata.Sized.M using (M)
open import Data.W.Sized using (W)
open import Data.Container hiding (μ) public

private
  variable
    s p : Level

-- The sized least and greatest fixpoints of a container.

μ : Container s p → Size → Set (s ⊔ p)
μ = W

ν : Container s p → Size → Set (s ⊔ p)
ν = M