open import Level.NP open import Data.Product.NP open import Control.Protocol.Core open import Control.Protocol.End module Control.Protocol.Lift a {ℓ} where liftᴾ : Proto_ ℓ → Proto_ (a ⊔ ℓ) liftᴾ end = end liftᴾ (com io P) = com io λ m → liftᴾ (P (lower {ℓ = a} m)) lift-proc : (P : Proto_ ℓ) → ⟦ P ⟧ → ⟦ liftᴾ P ⟧ lift-proc end end = end lift-proc (send P) (m , p) = lift m , lift-proc (P m) p lift-proc (recv P) p = λ { (lift m) → lift-proc (P m) (p m) }