------------------------------------------------------------------------
-- 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)