    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Indexed containers aka interaction structures aka polynomial
    -- functors. The notation and presentation here is closest to that of
    -- Hancock and Hyvernat in "Programming interfaces and basic topology"
    -- (2006/9).
    ------------------------------------------------------------------------

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

    module Data.Container.Indexed where

    open import Level using (Level; zero; _⊔_)
    open import Data.Product.Base as Prod hiding (map)
    open import Data.W.Indexed using (W)
    open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
    open import Function.Bundles using (_↔_; Inverse)
    open import Relation.Unary using (Pred; _⊆_)
    open import Relation.Binary.Core using (Rel; REL)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≗_; refl; trans; subst)

    ------------------------------------------------------------------------

    -- The type and its semantics ("extension").

    open import Data.Container.Indexed.Core public
    open Container public

    -- Abbreviation for the commonly used level one version of indexed
    -- containers.

    infix 5 _▷_

    _▷_ : Set → Set → Set₁
    I ▷ O = Container I O zero zero

    -- The least and greatest fixpoint.

    μ : ∀ {o c r} {O : Set o} → Container O O c r → Pred O _
    μ = W

    -- An equivalence relation is defined in Data.Container.Indexed.WithK.

    ------------------------------------------------------------------------
    -- Functoriality

    -- Indexed containers are functors.

    map : ∀ {i o c r ℓ₁ ℓ₂} {I : Set i} {O : Set o}
          (C : Container I O c r) {X : Pred I ℓ₁} {Y : Pred I ℓ₂} →
          X ⊆ Y → ⟦ C ⟧ X ⊆ ⟦ C ⟧ Y
    map _ f = Prod.map ⟨id⟩ (λ g → f ⟨∘⟩ g)

    -- Some properties are proved in Data.Container.Indexed.WithK.

    ------------------------------------------------------------------------
    -- Container morphisms

    module _ {i₁ i₂ o₁ o₂}
             {I₁ : Set i₁} {I₂ : Set i₂} {O₁ : Set o₁} {O₂ : Set o₂} where

      -- General container morphism.

      record ContainerMorphism {c₁ c₂ r₁ r₂ ℓ₁ ℓ₂}
             (C₁ : Container I₁ O₁ c₁ r₁) (C₂ : Container I₂ O₂ c₂ r₂)
             (f : I₁ → I₂) (g : O₁ → O₂)
             (_∼_ : Rel I₂ ℓ₁) (_≈_ : REL (Set r₂) (Set r₁) ℓ₂)
             (_·_ : ∀ {A B} → A ≈ B → A → B) :
             Set (i₁ ⊔ i₂ ⊔ o₁ ⊔ o₂ ⊔ c₁ ⊔ c₂ ⊔ r₁ ⊔ r₂ ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          command   : Command C₁ ⊆ Command C₂ ⟨∘⟩ g
          response  : ∀ {o} {c₁ : Command C₁ o} →
                      Response C₂ (command c₁) ≈ Response C₁ c₁
          coherent  : ∀ {o} {c₁ : Command C₁ o} {r₂ : Response C₂ (command c₁)} →
                      f (next C₁ c₁ (response · r₂)) ∼ next C₂ (command c₁) r₂

      open ContainerMorphism public

      -- Plain container morphism.

      _⇒[_/_]_ : ∀ {c₁ c₂ r₁ r₂} →
                 Container I₁ O₁ c₁ r₁ → (I₁ → I₂) → (O₁ → O₂) →
                 Container I₂ O₂ c₂ r₂ → Set _
      C₁ ⇒[ f / g ] C₂ = ContainerMorphism C₁ C₂ f g _≡_ (λ R₂ R₁ → R₂ → R₁) _$_

      -- Linear container morphism.

      _⊸[_/_]_ : ∀ {c₁ c₂ r₁ r₂} →
                 Container I₁ O₁ c₁ r₁ → (I₁ → I₂) → (O₁ → O₂) →
                 Container I₂ O₂ c₂ r₂ → Set _
      C₁ ⊸[ f / g ] C₂ = ContainerMorphism C₁ C₂ f g _≡_ _↔_
                                           (λ r₂↔r₁ r₂ → Inverse.to r₂↔r₁ r₂)

      -- Cartesian container morphism.

      _⇒C[_/_]_ : ∀ {c₁ c₂ r} →
                  Container I₁ O₁ c₁ r → (I₁ → I₂) → (O₁ → O₂) →
                  Container I₂ O₂ c₂ r → Set _
      C₁ ⇒C[ f / g ] C₂ = ContainerMorphism C₁ C₂ f g _≡_ (λ R₂ R₁ → R₂ ≡ R₁)
                                            (λ r₂≡r₁ r₂ → subst ⟨id⟩ r₂≡r₁ r₂)

    -- Degenerate cases where no reindexing is performed.

    module _ {i o c r} {I : Set i} {O : Set o} where

      infixr 8 _⇒_ _⊸_ _⇒C_

      _⇒_ : Rel (Container I O c r) _
      C₁ ⇒ C₂ = C₁ ⇒[ ⟨id⟩ / ⟨id⟩ ] C₂

      _⊸_ : Rel (Container I O c r) _
      C₁ ⊸ C₂ = C₁ ⊸[ ⟨id⟩ / ⟨id⟩ ] C₂

      _⇒C_ : Rel (Container I O c r) _
      C₁ ⇒C C₂ = C₁ ⇒C[ ⟨id⟩ / ⟨id⟩ ] C₂

    ------------------------------------------------------------------------
    -- Plain morphisms

    -- Interpretation of _⇒_.

    ⟪_⟫ : ∀ {i o c r ℓ} {I : Set i} {O : Set o} {C₁ C₂ : Container I O c r} →
          C₁ ⇒ C₂ → (X : Pred I ℓ) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X
    ⟪ m ⟫ X (c , k) = command m c , λ r₂ →
      subst X (coherent m) (k (response m r₂))

    module PlainMorphism {i o c r} {I : Set i} {O : Set o} where

      -- Identity.

      id : (C : Container I O c r) → C ⇒ C
      id _ = record
        { command  = ⟨id⟩
        ; response = ⟨id⟩
        ; coherent = refl
        }

      -- Composition.

      infixr 9 _∘_

      _∘_ : {C₁ C₂ C₃ : Container I O c r} →
            C₂ ⇒ C₃ → C₁ ⇒ C₂ → C₁ ⇒ C₃
      f ∘ g = record
        { command  = command  f ⟨∘⟩ command g
        ; response = response g ⟨∘⟩ response f
        ; coherent = coherent g ⟨ trans ⟩ coherent f
        }

      -- Identity commutes with ⟪_⟫.

      id-correct : ∀ {ℓ} {C : Container I O c r} → ∀ {X : Pred I ℓ} {o} →
                   ⟪ id C ⟫ X {o} ≗ ⟨id⟩
      id-correct _ = refl

      -- More properties are proved in Data.Container.Indexed.WithK.

    ------------------------------------------------------------------------
    -- Linear container morphisms

    module LinearMorphism
      {i o c r} {I : Set i} {O : Set o} {C₁ C₂ : Container I O c r}
      (m : C₁ ⊸ C₂)
      where

      morphism : C₁ ⇒ C₂
      morphism = record
        { command  = command m
        ; response = Inverse.to (response m)
        ; coherent = coherent m
        }

      ⟪_⟫⊸ : ∀ {ℓ} (X : Pred I ℓ) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X
      ⟪_⟫⊸ = ⟪ morphism ⟫

    open LinearMorphism public using (⟪_⟫⊸)

    ------------------------------------------------------------------------
    -- Cartesian morphisms

    module CartesianMorphism
      {i o c r} {I : Set i} {O : Set o} {C₁ C₂ : Container I O c r}
      (m : C₁ ⇒C C₂)
      where

      morphism : C₁ ⇒ C₂
      morphism = record
        { command  = command m
        ; response = subst ⟨id⟩ (response m)
        ; coherent = coherent m
        }

      ⟪_⟫C : ∀ {ℓ} (X : Pred I ℓ) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X
      ⟪_⟫C = ⟪ morphism ⟫

    open CartesianMorphism public using (⟪_⟫C)

    ------------------------------------------------------------------------
    -- All and any

    -- □ and ◇ are defined in the core module.

    module _ {i o c r ℓ₁ ℓ₂} {I : Set i} {O : Set o} (C : Container I O c r)
             {X : Pred I ℓ₁} {P Q : Pred (Σ I X) ℓ₂} where

      -- All.

      □-map : P ⊆ Q → □ C P ⊆ □ C Q
      □-map P⊆Q = _⟨∘⟩_ P⊆Q

      -- Any.

      ◇-map : P ⊆ Q → ◇ C P ⊆ ◇ C Q
      ◇-map P⊆Q = Prod.map ⟨id⟩ P⊆Q

    -- Membership is defined in Data.Container.Indexed.WithK.