{-# OPTIONS --without-K #-}
open import Function.NP
open import Type
open import Level.NP
open import Data.Product.NP using (Σ; _×_; _,_) renaming (proj₁ to fst)
open import Data.One using (𝟙)
open import Relation.Binary.PropositionalEquality.NP using (_≡_; !_; _∙_; refl; ap; coe; coe!)
open import Function.Extensionality
open import HoTT
open import Data.ShapePolymorphism
open Equivalences
open import Control.Protocol.InOut
module Control.Protocol.Core where
open import Control.Protocol.End public
module _ ℓ where
U = ★_ ℓ
U⟦_⟧ = id
data Proto_ : ★_(ₛ ℓ) where
end : Proto_
com : (io : InOut){M : U}(P : U⟦ M ⟧ → Proto_) → Proto_
Proto : ★₁
Proto = Proto_ ₀
Proto₀ = Proto
Proto₁ = Proto_ ₁
pattern recv P = com In P
pattern send P = com Out P
module _ {{_ : FunExt}} where
com= : ∀ {io₀ io₁}(io= : io₀ ≡ io₁)
{M₀ M₁ : ★}(M= : M₀ ≡ M₁)
{P₀ P₁}(P= : (m₀ : M₀) → P₀ m₀ ≡ P₁ (coe M= m₀))
→ com io₀ P₀ ≡ com io₁ P₁
com= refl refl P= = ap (com _) (λ= P=)
module _ {io₀ io₁}(io= : io₀ ≡ io₁)
{M₀ M₁}(M≃ : M₀ ≃ M₁)
{P₀ : M₀ → Proto}{P₁ : M₁ → Proto}
(P= : ∀ m₀ → P₀ m₀ ≡ P₁ (–> M≃ m₀))
{{_ : UA}} where
com≃ : com io₀ P₀ ≡ com io₁ P₁
com≃ = com= io= (ua M≃) λ m → P= m ∙ ap P₁ (! coe-β M≃ m)
module _ io {M N}(P : M × N → Proto)
where
com₂ : Proto
com₂ = com io λ m → com io λ n → P (m , n)
send= = com= {Out} refl
send≃ = com≃ {Out} refl
recv= = com= {In} refl
recv≃ = com≃ {In} refl
com=′ : ∀ io {M}{P₀ P₁ : M → Proto}(P= : ∀ m → P₀ m ≡ P₁ m) → com io P₀ ≡ com io P₁
com=′ io = com= refl refl
send=′ : ∀ {M}{P₀ P₁ : M → Proto}(P= : ∀ m → P₀ m ≡ P₁ m) → send P₀ ≡ send P₁
send=′ = send= refl
recv=′ : ∀ {M}{P₀ P₁ : M → Proto}(P= : ∀ m → P₀ m ≡ P₁ m) → recv P₀ ≡ recv P₁
recv=′ = recv= refl
pattern recvE M P = com In {M} P
pattern sendE M P = com Out {M} P
recv☐ : {M : ★}(P : ..(_ : M) → Proto) → Proto
recv☐ P = recv (λ { [ m ] → P m })
send☐ : {M : ★}(P : ..(_ : M) → Proto) → Proto
send☐ P = send (λ { [ m ] → P m })
dual : Proto → Proto
dual end = end
dual (com io P) = com (dualᴵᴼ io) λ m → dual (P m)
source-of : Proto → Proto
source-of end = end
source-of (com _ P) = send λ m → source-of (P m)
sink-of : Proto → Proto
sink-of = dual ∘ source-of
data IsSource : Proto → ★₁ where
end : IsSource end
send' : ∀ {M P} (PT : (m : M) → IsSource (P m)) → IsSource (send P)
data IsSink : Proto → ★₁ where
end : IsSink end
recv' : ∀ {M P} (PT : (m : M) → IsSink (P m)) → IsSink (recv P)
data Proto☐ : Proto → ★₁ where
end : Proto☐ end
com : ∀ io {M P} (P☐ : ∀ (m : ☐ M) → Proto☐ (P m)) → Proto☐ (com io P)
⟦_⟧ : ∀ {ℓ} → Proto_ ℓ → ★_ ℓ
⟦ end ⟧ = End
⟦ com io P ⟧ = ⟦ io ⟧ᴵᴼ _ λ m → ⟦ P m ⟧
⟦_⊥⟧ : Proto → ★
⟦ P ⊥⟧ = ⟦ dual P ⟧
Log : Proto → ★
Log P = ⟦ source-of P ⟧
Sink : Proto → ★
Sink P = ⟦ sink-of P ⟧
sink : ∀ P → Sink P
sink end = _
sink (com _ P) x = sink (P x)
telecom : ∀ P → ⟦ P ⟧ → ⟦ P ⊥⟧ → Log P
telecom end _ _ = _
telecom (recv P) p (m , q) = m , telecom (P m) (p m) q
telecom (send P) (m , p) q = m , telecom (P m) p (q m)
send′ : ★ → Proto → Proto
send′ M P = send λ (_ : M) → P
recv′ : ★ → Proto → Proto
recv′ M P = recv λ (_ : M) → P
module _ {{_ : FunExt}} where
dual-involutive : ∀ P → dual (dual P) ≡ P
dual-involutive end = refl
dual-involutive (com io P) = com= (dualᴵᴼ-involutive io) refl λ m → dual-involutive (P m)
dual-equiv : Is-equiv dual
dual-equiv = self-inv-is-equiv dual-involutive
dual-inj : ∀ {P Q} → dual P ≡ dual Q → P ≡ Q
dual-inj = Is-equiv.injective dual-equiv
source-of-idempotent : ∀ P → source-of (source-of P) ≡ source-of P
source-of-idempotent end = refl
source-of-idempotent (com _ P) = com= refl refl λ m → source-of-idempotent (P m)
source-of-dual-oblivious : ∀ P → source-of (dual P) ≡ source-of P
source-of-dual-oblivious end = refl
source-of-dual-oblivious (com _ P) = com= refl refl λ m → source-of-dual-oblivious (P m)
module _ {{_ : FunExt}} where
sink-contr : ∀ P s → sink P ≡ s
sink-contr end s = refl
sink-contr (com _ P) s = λ= λ m → sink-contr (P m) (s m)
Sink-is-contr : ∀ P → Is-contr (Sink P)
Sink-is-contr P = sink P , sink-contr P
𝟙≃Sink : ∀ P → 𝟙 ≃ Sink P
𝟙≃Sink P = Is-contr-to-Is-equiv.𝟙≃ (Sink-is-contr P)
dual-Log : ∀ P → Log (dual P) ≡ Log P
dual-Log = ap ⟦_⟧ ∘ source-of-dual-oblivious