```------------------------------------------------------------------------
-- The Agda standard library
--
-- Container combinators
------------------------------------------------------------------------

module Data.Container.Combinator where

open import Data.Container
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_)
open import Data.Sum renaming (_⊎_ to _⟨⊎⟩_)
open import Data.Unit using (⊤)
open import Function as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_)
open import Function.Inverse using (_↔_)
open import Level
open import Relation.Binary.PropositionalEquality as P
using (_≗_; refl)

------------------------------------------------------------------------
-- Combinators

-- Identity.

id : ∀ {c} → Container c
id = Lift ⊤ ▷ F.const (Lift ⊤)

-- Constant.

const : ∀ {c} → Set c → Container c
const X = X ▷ F.const (Lift ⊥)

-- Composition.

infixr 9 _∘_

_∘_ : ∀ {c} → Container c → Container c → Container c
C₁ ∘ C₂ = ⟦ C₁ ⟧ (Shape C₂) ▷ ◇ (Position C₂)

-- Product. (Note that, up to isomorphism, this is a special case of
-- indexed product.)

infixr 2 _×_

_×_ : ∀ {c} → Container c → Container c → Container c
C₁ × C₂ =
(Shape C₁ ⟨×⟩ Shape C₂) ▷
uncurry (λ s₁ s₂ → Position C₁ s₁ ⟨⊎⟩ Position C₂ s₂)

-- Indexed product.

Π : ∀ {c} {I : Set c} → (I → Container c) → Container c
Π C = (∀ i → Shape (C i)) ▷ λ s → ∃ λ i → Position (C i) (s i)

-- Sum. (Note that, up to isomorphism, this is a special case of
-- indexed sum.)

infixr 1 _⊎_

_⊎_ : ∀ {c} → Container c → Container c → Container c
C₁ ⊎ C₂ = (Shape C₁ ⟨⊎⟩ Shape C₂) ▷ [ Position C₁ , Position C₂ ]

-- Indexed sum.

Σ : ∀ {c} {I : Set c} → (I → Container c) → Container c
Σ C = (∃ λ i → Shape (C i)) ▷ λ s → Position (C (proj₁ s)) (proj₂ s)

-- Constant exponentiation. (Note that this is a special case of
-- indexed product.)

infix 0 const[_]⟶_

const[_]⟶_ : ∀ {c} → Set c → Container c → Container c
const[ X ]⟶ C = Π {I = X} (F.const C)

------------------------------------------------------------------------
-- Correctness proofs

-- I have proved some of the correctness statements under the
-- assumption of functional extensionality. I could have reformulated
-- the statements using suitable setoids, but I could not be bothered.

module Identity where

correct : ∀ {c} {X : Set c} → ⟦ id ⟧ X ↔ F.id X
correct {c} = record
{ to         = P.→-to-⟶ {a  = c} λ xs → proj₂ xs _
; from       = P.→-to-⟶ {b₁ = c} λ x → (_ , λ _ → x)
; inverse-of = record
{ left-inverse-of  = λ _ → refl
; right-inverse-of = λ _ → refl
}
}

module Constant (ext : ∀ {ℓ} → P.Extensionality ℓ ℓ) where

correct : ∀ {ℓ} (X : Set ℓ) {Y} → ⟦ const X ⟧ Y ↔ F.const X Y
correct X {Y} = record
{ to         = P.→-to-⟶ to
; from       = P.→-to-⟶ from
; inverse-of = record
{ right-inverse-of = λ _ → refl
; left-inverse-of  =
λ xs → P.cong (_,_ (proj₁ xs)) (ext (λ x → ⊥-elim (lower x)))
}
}
where
to : ⟦ const X ⟧ Y → X
to = proj₁

from : X → ⟦ const X ⟧ Y
from = < F.id , F.const (⊥-elim ∘′ lower) >

module Composition where

correct : ∀ {c} (C₁ C₂ : Container c) {X : Set c} →
⟦ C₁ ∘ C₂ ⟧ X ↔ (⟦ C₁ ⟧ ⟨∘⟩ ⟦ C₂ ⟧) X
correct C₁ C₂ {X} = record
{ to         = P.→-to-⟶ to
; from       = P.→-to-⟶ from
; inverse-of = record
{ left-inverse-of  = λ _ → refl
; right-inverse-of = λ _ → refl
}
}
where
to : ⟦ C₁ ∘ C₂ ⟧ X → ⟦ C₁ ⟧ (⟦ C₂ ⟧ X)
to ((s , f) , g) = (s , < f , curry g >)

from : ⟦ C₁ ⟧ (⟦ C₂ ⟧ X) → ⟦ C₁ ∘ C₂ ⟧ X
from (s , f) = ((s , proj₁ ⟨∘⟩ f) , uncurry (proj₂ ⟨∘⟩ f))

module Product (ext : ∀ {ℓ} → P.Extensionality ℓ ℓ) where

correct : ∀ {c} (C₁ C₂ : Container c) {X : Set c} →
⟦ C₁ × C₂ ⟧ X ↔ (⟦ C₁ ⟧ X ⟨×⟩ ⟦ C₂ ⟧ X)
correct {c} C₁ C₂ {X} = record
{ to         = P.→-to-⟶ to
; from       = P.→-to-⟶ from
; inverse-of = record
{ left-inverse-of  = from∘to
; right-inverse-of = λ _ → refl
}
}
where
to : ⟦ C₁ × C₂ ⟧ X → ⟦ C₁ ⟧ X ⟨×⟩ ⟦ C₂ ⟧ X
to ((s₁ , s₂) , f) = ((s₁ , f ⟨∘⟩ inj₁) , (s₂ , f ⟨∘⟩ inj₂))

from : ⟦ C₁ ⟧ X ⟨×⟩ ⟦ C₂ ⟧ X → ⟦ C₁ × C₂ ⟧ X
from ((s₁ , f₁) , (s₂ , f₂)) = ((s₁ , s₂) , [ f₁ , f₂ ])

from∘to : from ⟨∘⟩ to ≗ F.id
from∘to (s , f) =
P.cong (_,_ s) (ext {ℓ = c} [ (λ _ → refl) , (λ _ → refl) ])

module IndexedProduct where

correct : ∀ {c I} (C : I → Container c) {X : Set c} →
⟦ Π C ⟧ X ↔ (∀ i → ⟦ C i ⟧ X)
correct {I = I} C {X} = record
{ to         = P.→-to-⟶ to
; from       = P.→-to-⟶ from
; inverse-of = record
{ left-inverse-of  = λ _ → refl
; right-inverse-of = λ _ → refl
}
}
where
to : ⟦ Π C ⟧ X → ∀ i → ⟦ C i ⟧ X
to (s , f) = λ i → (s i , λ p → f (i , p))

from : (∀ i → ⟦ C i ⟧ X) → ⟦ Π C ⟧ X
from f = (proj₁ ⟨∘⟩ f , uncurry (proj₂ ⟨∘⟩ f))

module Sum where

correct : ∀ {c} (C₁ C₂ : Container c) {X : Set c} →
⟦ C₁ ⊎ C₂ ⟧ X ↔ (⟦ C₁ ⟧ X ⟨⊎⟩ ⟦ C₂ ⟧ X)
correct C₁ C₂ {X} = record
{ to         = P.→-to-⟶ to
; from       = P.→-to-⟶ from
; inverse-of = record
{ left-inverse-of  = from∘to
; right-inverse-of = [ (λ _ → refl) , (λ _ → refl) ]
}
}
where
to : ⟦ C₁ ⊎ C₂ ⟧ X → ⟦ C₁ ⟧ X ⟨⊎⟩ ⟦ C₂ ⟧ X
to (inj₁ s₁ , f) = inj₁ (s₁ , f)
to (inj₂ s₂ , f) = inj₂ (s₂ , f)

from : ⟦ C₁ ⟧ X ⟨⊎⟩ ⟦ C₂ ⟧ X → ⟦ C₁ ⊎ C₂ ⟧ X
from = [ Prod.map inj₁ F.id , Prod.map inj₂ F.id ]

from∘to : from ⟨∘⟩ to ≗ F.id
from∘to (inj₁ s₁ , f) = refl
from∘to (inj₂ s₂ , f) = refl

module IndexedSum where

correct : ∀ {c I} (C : I → Container c) {X : Set c} →
⟦ Σ C ⟧ X ↔ (∃ λ i → ⟦ C i ⟧ X)
correct {I = I} C {X} = record
{ to         = P.→-to-⟶ to
; from       = P.→-to-⟶ from
; inverse-of = record
{ left-inverse-of  = λ _ → refl
; right-inverse-of = λ _ → refl
}
}
where
to : ⟦ Σ C ⟧ X → ∃ λ i → ⟦ C i ⟧ X
to ((i , s) , f) = (i , (s , f))

from : (∃ λ i → ⟦ C i ⟧ X) → ⟦ Σ C ⟧ X
from (i , (s , f)) = ((i , s) , f)

module ConstantExponentiation where

correct : ∀ {c X} (C : Container c) {Y : Set c} →
⟦ const[ X ]⟶ C ⟧ Y ↔ (X → ⟦ C ⟧ Y)
correct C = IndexedProduct.correct (F.const C)
```