------------------------------------------------------------------------
-- The Agda standard library
--
-- Propertiers of any for containers
------------------------------------------------------------------------

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

module Data.Container.Morphism.Properties where

open import Level using (_⊔_; suc)
open import Function.Base as F using (_$_)
open import Data.Product.Base using (∃; proj₁; proj₂; _,_)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)

open import Data.Container.Core
open import Data.Container.Morphism
open import Data.Container.Relation.Binary.Equality.Setoid

-- Identity

module _ {s p} (C : Container s p) where

  id-correct : ∀ {x} {X : Set x} → ⟪ id C ⟫ {X = X} ≗ F.id
  id-correct x = P.refl

-- Composition.

module _ {s₁ s₂ s₃ p₁ p₂ p₃}
         {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} {C₃ : Container s₃ p₃}
         where

  ∘-correct : (f : C₂ ⇒ C₃) (g : C₁ ⇒ C₂) → ∀ {x} {X : Set x} →
              ⟪ f ∘ g ⟫ {X = X} ≗ (⟪ f ⟫ F.∘ ⟪ g ⟫)
  ∘-correct f g xs = P.refl

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} where

  -- Naturality.

  Natural : ∀ x e → (∀ {X : Set x} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X) →
            Set (s₁ ⊔ s₂ ⊔ p₁ ⊔ p₂ ⊔ suc (x ⊔ e))
  Natural x e m =
    ∀ {X : Set x} (Y : Setoid x e) → let module Y = Setoid Y in
    (f : X → Y.Carrier) (xs : ⟦ C₁ ⟧ X) →
    Eq Y C₂ (m $ map f xs) (map f $ m xs)

  -- Container morphisms are natural.

  natural : ∀ (m : C₁ ⇒ C₂) x e → Natural x e ⟪ m ⟫
  natural m x e Y f xs = refl Y C₂

module _ {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) where

  -- Natural transformations.

  NT : ∀ x e → Set (s₁ ⊔ s₂ ⊔ p₁ ⊔ p₂ ⊔ suc (x ⊔ e))
  NT x e = ∃ λ (m : ∀ {X : Set x} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X) → Natural x e m

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} where

  -- All natural functions of the right type are container morphisms.

  complete : ∀ {e} → (nt : NT C₁ C₂ p₁ e) →
      ∃ λ m → (X : Setoid p₁ e) → let module X = Setoid X in
      ∀ xs → Eq X C₂ (proj₁ nt xs) (⟪ m ⟫ xs)
  complete (nt , nat) =
    (m , λ X xs → nat X (proj₂ xs) (proj₁ xs , F.id)) where

    m : C₁ ⇒ C₂
    m .shape    = λ s → proj₁ (nt (s , F.id))
    m .position = proj₂ (nt (_ , F.id))