open import Prelude

module CCS.Hyp.Definition
  {r}
  (Name : Type r)
  (R : Type r)
  where

open import Hyper.Base
open import CCS.Act

Communicator : Type r
Communicator = (Maybe (Act Name) → R) ↬ (Maybe (Act Name) → R)

module _ (isSetR : isSet R) where
  isSet-Communicator : isSet Communicator
  isSet-Communicator x y x≡y₁ x≡y₂ i j .ι k m = isSetR (x .ι k m) (y .ι k m) (cong (λ x′ → x′ .ι k m) x≡y₁) (cong (λ x′ → x′ .ι k m) x≡y₂) i j