------------------------------------------------------------------------
-- 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`.