open import Type open import Data.Sum renaming (inj₁ to inl; inj₂ to inr; [_,_] to [inl:_,inr:_]) hiding ([_,_]′) open import Function open import Function.Extensionality open import Relation.Binary.PropositionalEquality open import Control.Protocol.Core module Control.Protocol.Extend where module _ {A : ★} (Aᴾ : A → Proto) where extend-send : Proto → Proto extend-send end = end extend-send (send P) = send [inl: (λ m → extend-send (P m)) ,inr: Aᴾ ] extend-send (recv P) = recv λ m → extend-send (P m) extend-recv : Proto → Proto extend-recv end = end extend-recv (recv P) = recv [inl: (λ m → extend-recv (P m)) ,inr: Aᴾ ] extend-recv (send P) = send λ m → extend-recv (P m) module _ {A : ★} (Aᴾ : A → Proto){{_ : FunExt}} where dual-extend-send : ∀ P → dual (extend-send Aᴾ P) ≡ extend-recv (dual ∘ Aᴾ) (dual P) dual-extend-send end = refl dual-extend-send (recv P) = send=′ λ m → dual-extend-send (P m) dual-extend-send (send P) = recv=′ [inl: (λ m → dual-extend-send (P m)) ,inr: (λ x → refl) ] data Abort : ★ where abort : Abort Abortᴾ : Abort → Proto Abortᴾ _ = end add-abort : Proto → Proto add-abort = extend-send Abortᴾ