    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Containers, based on the work of Abbott and others
    ------------------------------------------------------------------------

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

    open import Level using (Level; _⊔_)
    open import Data.W using (W)

    module Data.Container where

    ------------------------------------------------------------------------
    -- Re-exporting content to maintain backwards compatibility

    open import Data.Container.Core public
    open import Data.Container.Relation.Unary.Any
      using (◇) renaming (map to ◇-map) public
    open import Data.Container.Relation.Unary.All
      using (□) renaming (map to □-map) public
    open import Data.Container.Membership
      using (_∈_) public
    open import Data.Container.Relation.Binary.Pointwise
      using () renaming (Pointwise to Eq) public
    open import Data.Container.Relation.Binary.Pointwise.Properties
      using (refl; sym; trans) public
    open import Data.Container.Relation.Binary.Equality.Setoid
      using (isEquivalence; setoid) public
    open import Data.Container.Properties
      using () renaming (map-identity to identity; map-compose to composition) public
    open import Data.Container.Related public

    module Morphism where

      open import Data.Container.Morphism.Properties
        using (Natural; NT; natural; complete; id-correct; ∘-correct) public

      open import Data.Container.Morphism
        using (id; _∘_) public

    private
      variable
        s p : Level

    -- The least fixpoint of a container.

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

    -- The greatest fixpoint of a container can be found
    -- in `Data.Container.Fixpoints.Guarded` as it relies
    -- on the `guardedness` flag.

    -- You can find sized alternatives in `Data.Container.Fixpoints.Sized`
    -- as they rely on the unsafe flag `--sized-types`.