{-# 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 Type

module Control.Protocol.InOut where

data InOut : ★ where
  In Out : InOut

dualᴵᴼ : InOut → InOut
dualᴵᴼ In  = Out
dualᴵᴼ Out = In

dualᴵᴼ-involutive : ∀ io → dualᴵᴼ (dualᴵᴼ io) ≡ io
dualᴵᴼ-involutive In = refl
dualᴵᴼ-involutive Out = refl

dualᴵᴼ-equiv : Is-equiv dualᴵᴼ
dualᴵᴼ-equiv = self-inv-is-equiv dualᴵᴼ-involutive

dualᴵᴼ-inj : ∀ {x y} → dualᴵᴼ x ≡ dualᴵᴼ y → x ≡ y
dualᴵᴼ-inj = Is-equiv.injective dualᴵᴼ-equiv

⟦_⟧ᴵᴼ : InOut → ∀{ℓ}(M : ★_ ℓ)(P : M → ★_ ℓ) → ★_ ℓ
⟦_⟧ᴵᴼ In  = Π
⟦_⟧ᴵᴼ Out = Σ