module README where

-- Hyperfunction Definition

import Hyper.Base using (_↬_)

--------------------------------------------------------------------------------
-- Section 3
--------------------------------------------------------------------------------

--  3.2
-- =====

-- CCS Algebras
import CCS.Alg using (CCSAlg)

-- CCS Syntax
import CCS.Syntax using (P)

--  3.3
-- =====

-- The Communicator Type
import CCS.Hyp.Definition using (Communicator)

-- The Alg instance
import CCS.Hyp.Alg

-- Interpretation
import CCS.Hyp.Interp

--  3.4
-- =====

-- The Proc Model
import CCS.Proc

-- Lemma 3.9
import CCS.Homomorphism using (proc→com→proc)

-- Lemma 3.10
import CCS.Homomorphism.CtoP using (hom↓)

-- Lemma 3.11
import CCS.Homomorphism using (hom↑)

-- Theorem 3.12
import CCS.Homomorphism using (Comm-full-abstraction)

-- Lemma 3.14
import CCS.Hyp.SemiModel using (·⌊-decomp)

-- Lemma 3.15
import CCS.Homomorphism.CtoP using (⌊-hom↓)

-- Lemma 3.16
import CCS.Homomorphism.PtoC using (⌊-hom↑)