------------------------------------------------------------------------
-- 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`.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4