depsession2.agda

{-
import Data.Product
module depsession2 (open Data.Product) (let _² = λ A → A × A) (x : Set ²) where
y = _×_
-}
module depsession2 where

open import Type hiding (★)
open import Level.NP
open import Function.NP
open import Data.Zero
open import Data.One
open import Data.Two
open import Data.W
open import Data.Nat hiding (_⊔_)
open import Data.Product.NP
open import Data.Sum
open import Relation.Binary.PropositionalEquality
import Function.Inverse.NP as Inv -- using (module Inv)
open Inv using (_↔_)
open import Function.Related.TypeIsomorphisms.NP

record W⊥ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  field
    sup⊥ : (x : A) → Σ (B x) (λ y → W⊥ A B)

data U : ★₁ where
  `Π `Σ `W : (A : ★₀) (b : A → U) → U
  _`⊗_ _`⅋_ : (a b : U) → U
  `_ : (A : ★₀) → U

El : U → ★₀
El (` A)    = A
El (`Π A b) = (x : A) → El (b x)
El (`Σ A b) = Σ A λ x → El (b x)
El (`W A b) = W A λ x → El (b x)
El (a `⊗ b) = El a × El b
El (a `⅋ b) = El a → El b

infix 5 _`&_ _`⊕_

-- no good...
-- infix 5 _`×_
--_`×_ : (a b : U) → U
--a `× b = `Σ a (λ x → b)

_`&_ : (a b : U) → U
a `& b = `Π 𝟚 [0: a 1: b ]

_`⊕_ : (a b : U) → U
a `⊕ b = `Σ 𝟚 [0: a 1: b ]

open import LL hiding (_⊥; _↔_; _⊥-inv; a; b; c; d)

{-
A ⊗ B 'times', output/send A then behave as B
A ⅋ B 'par', input/receive A then behave as B
A ⊕ B 'plus', select from A or B
A & B 'with', offer choice of A or B
`1    unit for ⊗
`⊤    unit for ⅋
`0    unit for ⊕
`⊥    unit for &
-}
⟦_⟧ : Form → U
⟦ `1 ⟧ = ` 𝟙 -- same as `Σ 𝟙
⟦ `⊤ ⟧ = ` 𝟙 -- same as 
⟦ `0 ⟧ = `Σ 𝟘 𝟘-elim
⟦ `⊥ ⟧ = `Π 𝟘 𝟘-elim
⟦ A ⊗ B ⟧ = ⟦ A ⟧ `⊗ ⟦ B ⟧
⟦ A ⅋ B ⟧ = ⟦ A ⟧ `⅋ ⟦ B ⟧
⟦ A ⊕ B ⟧ = ⟦ A ⟧ `⊕ ⟦ B ⟧
⟦ A & B ⟧ = ⟦ A ⟧ `& ⟦ B ⟧
⟦ ‼ x ⟧ = ⟦ x ⟧ -- erased
⟦ ⁇ x ⟧ = ⟦ x ⟧ -- erased

`Strategy : (Q : ★₀) (R : Q → ★₀) (A : U) (n : ℕ) → U
`Strategy Q R A zero    = A                        -- no fuel, you have to return!
`Strategy Q R A (suc n) = A `⊕                     -- the client has the choice to return now or continue
                          `Σ Q λ q →               -- client sends a query
                              `Π (R q) λ r →       -- and waits for a response of a type depending on q
                                 `Strategy Q R A n -- the client continue with his strategy

infix 11 _⊥
_⊥ : U → U
(`Π A b)⊥ = `Σ A (λ x → (b x)⊥)
(`Σ B b)⊥ = `Π B (λ x → (b x)⊥)
(a `⊗ b)⊥ = (a ⊥) `⅋ (b ⊥)
(a)⊥      = a

⟨_`&_⟩⊥ : (a b : U) → El ((a `& b)⊥) ↔ El (a ⊥ `⊕ b ⊥)
⟨ _ `& _ ⟩⊥ = second-iso [0: Inv.id 1: Inv.id ]

-- requires function extenstionality
module _ (extU : {b : 𝟚 → U} {f g : Π 𝟚 (El ∘ b)} → (∀ x → f x ≡ g x) → f ≡ g) where

    ⟨_`⊕_⟩⊥ : (a b : U) → El ((a `⊕ b)⊥) ↔ El (a ⊥ `& b ⊥)
    ⟨ a `⊕ b ⟩⊥ = fiber-iso (extU {λ x → [0: a 1: b ] x ⊥}) (extU {[0: a ⊥ 1: b ⊥ ]}) [0: Inv.id 1: Inv.id ]

    {-
-- requires function extenstionality
module _ (extU : {A : ★₀} {f g : A → U} → (∀ x → f x ≡ g x) → f ≡ g) where
    _⊥-inv : ∀ a → (a ⊥)⊥ ≡ a
    `Π a b ⊥-inv = cong (`Π a) (extU λ x → b x ⊥-inv)
    `Σ a b ⊥-inv = cong (`Σ a) (extU λ x → b x ⊥-inv)
    `W a b ⊥-inv = refl
    (` _) ⊥-inv = refl

Run : (a : U) → El a → El (a ⊥) → ★₀
Run (`Π A b) p       (x , q) = Run (b x) (p x) q
Run (`Σ A b) (x , p) q       = Run (b x) p (q x)
Run a        x       y       = El a × El a

run : (a : U) (p : El a) (q : El (a ⊥)) → Run a p q
run (`Π a b)   p          (x , q) = run (b x) (p x) q
run (`Σ a b)   (x , p)    q       = run (b x) p (q x)
run (`W _ _)   x          y       = x , y
run (` a)      x          y       = x , y

module Next (U : ★₀)
            (El : U → ★₀)
            (_⊥ : U → U)
            (Run : (a : U) → El a → El (a ⊥) → ★₀)
            (run : (a : U) (p : El a) (q : El (a ⊥)) → Run a p q)
            where
    data Uₛ : ★₁ where
      `Π `Σ `W : (A : ★₀) (b : A → Uₛ) → Uₛ
      `U : Uₛ
      `_ : U → Uₛ

    Elₛ : Uₛ → ★₀
    Elₛ (`Π A b) = (x : A) → Elₛ (b x)
    Elₛ (`Σ A b) = Σ A λ x → Elₛ (b x)
    Elₛ (`W A b) = W A λ x → Elₛ (b x)
    Elₛ `U       = U
    Elₛ (` u)    = El u

    infix 11 _⊥ₛ
    _⊥ₛ : Uₛ → Uₛ
    (`Π A b)⊥ₛ = `Σ A λ x → (b x)⊥ₛ
    (`Σ A b)⊥ₛ = `Π A λ x → (b x)⊥ₛ
    (` u)⊥ₛ    = ` (u ⊥)
    (uₛ)⊥ₛ     = uₛ

    Runₛ : (a : Uₛ) → Elₛ a → Elₛ (a ⊥ₛ) → ★₀
    Runₛ (`Π A b) p       (x , q) = Runₛ (b x) (p x) q
    Runₛ (`Σ A b) (x , p) q       = Runₛ (b x) p (q x)
    Runₛ (` u)    x       y       = Run u x y
    Runₛ a        x       y       = Elₛ a × Elₛ a

    runₛ : (a : Uₛ) (p : Elₛ a) (q : Elₛ (a ⊥ₛ)) → Runₛ a p q
    runₛ (`Π a b) p       (x , q) = runₛ (b x) (p x) q
    runₛ (`Σ a b) (x , p) q       = runₛ (b x) p (q x)
    runₛ (` a)    x       y       = run a x y
    runₛ (`W _ _) x       y       = x , y
    runₛ `U       x       y       = x , y
-- -}
-- -}
-- -}
-- -}