------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed container combinators
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Container.Indexed.Combinator where
open import Axiom.Extensionality.Propositional using (Extensionality)
open import Data.Container.Indexed using (Container; _◃_/_; ⟦_⟧;
Command; Response; ◇; next)
open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
open import Data.Unit.Polymorphic.Base using (⊤)
open import Data.Product.Base as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_)
open import Data.Sum.Base renaming (_⊎_ to _⟨⊎⟩_)
open import Data.Sum.Relation.Unary.All as All using (All)
open import Function.Base as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_)
open import Function.Bundles using (mk↔ₛ′)
open import Function.Indexed.Bundles using (_↔ᵢ_)
open import Level using (Level; _⊔_)
open import Relation.Unary using (Pred; _⊆_; _∪_; _∩_; ⋃; ⋂)
renaming (_⟨×⟩_ to _⟪×⟫_; _⟨⊙⟩_ to _⟪⊙⟫_; _⟨⊎⟩_ to _⟪⊎⟫_)
open import Relation.Binary.PropositionalEquality.Core
using (_≗_; refl; cong)
private
variable
ℓ ℓ₁ ℓ₂ i j k o c c₁ c₂ r r₁ r₂ x z : Level
I J K O X Z : Set _
------------------------------------------------------------------------
-- Combinators
-- Identity.
id : Container O O c r
id = F.const ⊤ ◃ F.const ⊤ / (λ {o} _ _ → o)
-- Constant.
const : Pred O c → Container I O c r
const X = X ◃ F.const ⊥ / F.const ⊥-elim
-- Composition.
infixr 9 _∘_
_∘_ : Container J K c₁ r₁ → Container I J c₂ r₂ → Container I K _ _
C₁ ∘ C₂ = C ◃ R / n
where
C : ∀ k → Set _
C = ⟦ C₁ ⟧ (Command C₂)
R : ∀ {k} → ⟦ C₁ ⟧ (Command C₂) k → Set _
R (c , k) = ◇ C₁ {X = Command C₂} (Response C₂ ⟨∘⟩ proj₂) (_ , c , k)
n : ∀ {k} (c : ⟦ C₁ ⟧ (Command C₂) k) → R c → _
n (_ , f) (r₁ , r₂) = next C₂ (f r₁) r₂
-- Duality.
_^⊥ : Container I O c r → Container I O (c ⊔ r) c
(C ^⊥) .Command o = (c : C .Command o) → C .Response c
(C ^⊥) .Response {o} _ = C .Command o
(C ^⊥) .next f c = C .next c (f c)
-- Strength.
infixl 3 _⋊_
_⋊_ : Container I O c r → (Z : Set z) → Container (I ⟨×⟩ Z) (O ⟨×⟩ Z) c r
(C ⋊ Z) .Command (o , z) = C .Command o
(C ⋊ Z) .Response = C .Response
(C ⋊ Z) .next {o , z} c r = C .next c r , z
infixr 3 _⋉_
_⋉_ : (Z : Set z) → Container I O c r → Container (Z ⟨×⟩ I) (Z ⟨×⟩ O) c r
(Z ⋉ C) .Command (z , o) = C .Command o
(Z ⋉ C) .Response = C .Response
(Z ⋉ C) .next {z , o} c r = z , C .next c r
-- Product. (Note that, up to isomorphism, and ignoring universe level
-- issues, this is a special case of indexed product.)
infixr 2 _×_
_×_ : Container I O c₁ r₁ → Container I O c₂ r₂ → Container I O _ _
(C₁ ◃ R₁ / n₁) × (C₂ ◃ R₂ / n₂) = record
{ Command = C₁ ∩ C₂
; Response = R₁ ⟪⊙⟫ R₂
; next = λ { (c₁ , c₂) → [ n₁ c₁ , n₂ c₂ ] }
}
-- Indexed product.
Π : (X → Container I O c r) → Container I O _ _
Π {X = X} C = record
{ Command = ⋂ X (Command ⟨∘⟩ C)
; Response = ⋃[ x ∶ X ] λ c → Response (C x) (c x)
; next = λ { c (x , r) → next (C x) (c x) r }
}
-- Sum. (Note that, up to isomorphism, and ignoring universe level
-- issues, this is a special case of indexed sum.)
infixr 1 _⊎_ _⊎′_
_⊎_ : Container I O c₁ r₁ → Container I O c₂ r₂ → Container I O _ _
(C₁ ⊎ C₂) .Command = C₁ .Command ∪ C₂ .Command
(C₁ ⊎ C₂) .Response = All (C₁ .Response) (C₂ .Response)
(C₁ ⊎ C₂) .next = All.[ C₁ .next , C₂ .next ]
-- A simplified version for responses at the same level r:
_⊎′_ : Container I O c₁ r → Container I O c₂ r → Container I O _ r
(C₁ ◃ R₁ / n₁) ⊎′ (C₂ ◃ R₂ / n₂) = record
{ Command = C₁ ∪ C₂
; Response = [ R₁ , R₂ ]
; next = [ n₁ , n₂ ]
}
-- Indexed sum.
Σ : (X → Container I O c r) → Container I O _ r
Σ {X = X} C = record
{ Command = ⋃ X (Command ⟨∘⟩ C)
; Response = λ { (x , c) → Response (C x) c }
; next = λ { (x , c) r → next (C x) c r }
}
-- Constant exponentiation. (Note that this is a special case of
-- indexed product.)
infix 0 const[_]⟶_
const[_]⟶_ : (X : Set ℓ) → Container I O c r → Container I O _ _
const[ X ]⟶ C = Π {X = X} (F.const C)
------------------------------------------------------------------------
-- Correctness proofs
module Identity where
correct : {X : Pred O ℓ} → ⟦ id {c = c}{r} ⟧ X ↔ᵢ F.id X
correct {X = X} = mk↔ₛ′ to from (λ _ → refl) (λ _ → refl)
where
to : ∀ {x} → ⟦ id ⟧ X x → F.id X x
to xs = proj₂ xs _
from : ∀ {x} → F.id X x → ⟦ id ⟧ X x
from x = (_ , λ _ → x)
module Constant (ext : ∀ {ℓ} → Extensionality ℓ ℓ) where
correct : (X : Pred O ℓ₁) {Y : Pred O ℓ₂} → ⟦ const X ⟧ Y ↔ᵢ F.const X Y
correct X {Y} = mk↔ₛ′ to from (λ _ → refl) to∘from
where
to : ⟦ const X ⟧ Y ⊆ X
to = proj₁
from : X ⊆ ⟦ const X ⟧ Y
from = < F.id , F.const ⊥-elim >
to∘from : _
to∘from xs = cong (proj₁ xs ,_) (ext ⊥-elim)
module Duality where
correct : (C : Container I O c r) (X : Pred I ℓ) →
⟦ C ^⊥ ⟧ X ↔ᵢ (λ o → (c : Command C o) → ∃ λ r → X (next C c r))
correct C X = mk↔ₛ′ (λ { (f , g) → < f , g > }) (λ f → proj₁ ⟨∘⟩ f , proj₂ ⟨∘⟩ f)
(λ _ → refl) (λ _ → refl)
module Composition where
correct : (C₁ : Container J K c r) (C₂ : Container I J c r) →
{X : Pred I ℓ} → ⟦ C₁ ∘ C₂ ⟧ X ↔ᵢ (⟦ C₁ ⟧ ⟨∘⟩ ⟦ C₂ ⟧) X
correct C₁ C₂ {X} = mk↔ₛ′ to from (λ _ → refl) (λ _ → refl)
where
to : ⟦ C₁ ∘ C₂ ⟧ X ⊆ ⟦ C₁ ⟧ (⟦ C₂ ⟧ X)
to ((c , f) , g) = (c , < f , curry g >)
from : ⟦ C₁ ⟧ (⟦ C₂ ⟧ X) ⊆ ⟦ C₁ ∘ C₂ ⟧ X
from (c , f) = ((c , proj₁ ⟨∘⟩ f) , uncurry (proj₂ ⟨∘⟩ f))
module Product (ext : ∀ {ℓ} → Extensionality ℓ ℓ) where
correct : (C₁ C₂ : Container I O c r) {X : Pred I _} →
⟦ C₁ × C₂ ⟧ X ↔ᵢ (⟦ C₁ ⟧ X ∩ ⟦ C₂ ⟧ X)
correct C₁ C₂ {X} = mk↔ₛ′ to from (λ _ → refl) from∘to
where
to : ⟦ C₁ × C₂ ⟧ X ⊆ ⟦ C₁ ⟧ X ∩ ⟦ C₂ ⟧ X
to ((c₁ , c₂) , k) = ((c₁ , k ⟨∘⟩ inj₁) , (c₂ , k ⟨∘⟩ inj₂))
from : ⟦ C₁ ⟧ X ∩ ⟦ C₂ ⟧ X ⊆ ⟦ C₁ × C₂ ⟧ X
from ((c₁ , k₁) , (c₂ , k₂)) = ((c₁ , c₂) , [ k₁ , k₂ ])
from∘to : from ⟨∘⟩ to ≗ F.id
from∘to (c , _) =
cong (c ,_) (ext [ (λ _ → refl) , (λ _ → refl) ])
module IndexedProduct where
correct : (C : X → Container I O c r) {Y : Pred I ℓ} →
⟦ Π C ⟧ Y ↔ᵢ ⋂[ x ∶ X ] ⟦ C x ⟧ Y
correct {X = X} C {Y} = mk↔ₛ′ to from (λ _ → refl) (λ _ → refl)
where
to : ⟦ Π C ⟧ Y ⊆ ⋂[ x ∶ X ] ⟦ C x ⟧ Y
to (c , k) = λ x → (c x , λ r → k (x , r))
from : ⋂[ x ∶ X ] ⟦ C x ⟧ Y ⊆ ⟦ Π C ⟧ Y
from f = (proj₁ ⟨∘⟩ f , uncurry (proj₂ ⟨∘⟩ f))
module Sum (ext : ∀ {ℓ₁ ℓ₂} → Extensionality ℓ₁ ℓ₂) where
correct : (C₁ C₂ : Container I O c r) {X : Pred I ℓ} →
⟦ C₁ ⊎ C₂ ⟧ X ↔ᵢ (⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X)
correct C₁ C₂ {X} = mk↔ₛ′ to from to∘from from∘to
where
to : ⟦ C₁ ⊎ C₂ ⟧ X ⊆ ⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X
to (inj₁ c₁ , k) = inj₁ (c₁ , λ r → k (All.inj₁ r))
to (inj₂ c₂ , k) = inj₂ (c₂ , λ r → k (All.inj₂ r))
from : ⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X ⊆ ⟦ C₁ ⊎ C₂ ⟧ X
from (inj₁ (c , f)) = inj₁ c , λ{ (All.inj₁ r) → f r}
from (inj₂ (c , f)) = inj₂ c , λ{ (All.inj₂ r) → f r}
from∘to : from ⟨∘⟩ to ≗ F.id
from∘to (inj₁ _ , _) = cong (inj₁ _ ,_) (ext λ{ (All.inj₁ r) → refl})
from∘to (inj₂ _ , _) = cong (inj₂ _ ,_) (ext λ{ (All.inj₂ r) → refl})
to∘from : to ⟨∘⟩ from ≗ F.id
to∘from = [ (λ _ → refl) , (λ _ → refl) ]
module Sum′ where
correct : (C₁ C₂ : Container I O c r) {X : Pred I ℓ} →
⟦ C₁ ⊎′ C₂ ⟧ X ↔ᵢ (⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X)
correct C₁ C₂ {X} = mk↔ₛ′ to from to∘from from∘to
where
to : ⟦ C₁ ⊎′ C₂ ⟧ X ⊆ ⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X
to (inj₁ c₁ , k) = inj₁ (c₁ , k)
to (inj₂ c₂ , k) = inj₂ (c₂ , k)
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₁ _ , _) = refl
from∘to (inj₂ _ , _) = refl
to∘from : to ⟨∘⟩ from ≗ F.id
to∘from = [ (λ _ → refl) , (λ _ → refl) ]
module IndexedSum where
correct : (C : X → Container I O c r) {Y : Pred I ℓ} →
⟦ Σ C ⟧ Y ↔ᵢ ⋃[ x ∶ X ] ⟦ C x ⟧ Y
correct {X = X} C {Y} = mk↔ₛ′ to from (λ _ → refl) (λ _ → refl)
where
to : ⟦ Σ C ⟧ Y ⊆ ⋃[ x ∶ X ] ⟦ C x ⟧ Y
to ((x , c) , k) = (x , (c , k))
from : ⋃[ x ∶ X ] ⟦ C x ⟧ Y ⊆ ⟦ Σ C ⟧ Y
from (x , (c , k)) = ((x , c) , k)
module ConstantExponentiation where
correct : (C : Container I O c r) {Y : Pred I ℓ} →
⟦ const[ X ]⟶ C ⟧ Y ↔ᵢ (⋂ X (F.const (⟦ C ⟧ Y)))
correct C {Y} = IndexedProduct.correct (F.const C) {Y}