{-# OPTIONS --no-termination-check  --lossy-unification #-}

open import Prelude hiding (P; A)

module CCS.Homomorphism where

private
  A : Type
  A = ℕ

open import CCS.Alg
open import CCS.SemiModel
import CCS.Proc as ℙ
open ℙ using (Proc; procAlg; procMod; ⟪_⟫; isSetProc; ↯; proc∘↯)
open import Algebra

open import Data.Set renaming (⟦_⟧ to 𝒦⟦_⟧)

open import Hyper.Base
open import CCS.Hyp.Definition A (Proc A)

open CCSAlg ⦃ ... ⦄
open CCSSemiModel ⦃ ... ⦄

instance
  _ : CCSAlg (Proc A)
  _ = procAlg

instance
  _ : CCSSemiModel (Proc A)
  _ = procMod

open import CCS.Hyp.Properties {R = Proc A} procMod hiding (⊕⌊)

instance
  _ : CCSAlg Communicator
  _ = hypAlg

instance
  _ : CCSSemiModel Communicator
  _ = hypMod


open import CCS.Hyp.Interp {R = Proc A} procAlg ⦃ it ⦄

open import CCS.Homomorphism.PtoC
open import CCS.Homomorphism.CtoP

proc→com→proc : ∀ p → ⟦ ⟦ p ⟧↑ ⟧↓ ≡ p
proc→com→proc p = 𝒦⟦ alg ⟧ (↯ p) ⨾ proc∘↯ p
  where
  alg : Ψ[ p ⦂ 𝒦 (Act A × Proc A) ] ↦ ⟦ ⟦ ⟪ p ⟫ ⟧↑ ⟧↓ ≡ ⟪ p ⟫
  alg .snd = prop-coh λ xs → isSetProc _ _
  alg .fst ∅ = refl
  alg .fst ⟅ a , p′ ⟆ = cong (λ e → ⟪ ⟅ a , e ⟆ ⟫) (proc→com→proc p′) 
  alg .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) =
    ⟦ ⟦ ⟪ xs ⟫ ⟧↑ ⊕ ⟦ ⟪ ys ⟫ ⟧↑ ⟧↓ ≡˘⟨ ⊕-hom↓ ⟦ ⟪ xs ⟫ ⟧↑ ⟦ ⟪ ys ⟫ ⟧↑ ⟩
    ⟦ ⟦ ⟪ xs ⟫ ⟧↑ ⟧↓ ⊕ ⟦ ⟦ ⟪ ys ⟫ ⟧↑ ⟧↓ ≡⟨ cong₂ _⊕_ P⟨xs⟩ P⟨ys⟩ ⟩
    ⟪ xs ∪ ys ⟫ ∎

⟦⟧↑-inj : Injective ⟦_⟧↑
⟦⟧↑-inj {x = x} {y} p = sym (proc→com→proc x) ⨾ cong ⟦_⟧↓ p ⨾ proc→com→proc y

hom↑ : (p : P A) → ⟦ ⟦ p ⟧ₚ ⟧↑ ≡ ⟦ p ⟧ᶜ
hom↑ p =
  ⟦ ⟦ p ⟧ₚ ⟧↑ ≡˘⟨ cong ⟦_⟧↑ (⌊𝟘 ⟦ p ⟧ₚ) ⟩
  ⟦ ⟦ p ⟧ₚ ⌊ 𝟘 ⟧↑ ≡⟨ ⌊-hom↑ [] p 𝟘 ⟩
  ⟦ p ⟧ᶜ ⌊ 𝟘 ≡⟨ ⌊𝟘 ⟦ p ⟧ᶜ ⟩
  ⟦ p ⟧ᶜ ∎


open import CCS.Bisimilar

postulate Proc-full-abstraction : (p q : P A) → (p ≈ q) ⟷ (⟦ p ⟧ ≡ (⟦ q ⟧ ⦂ Proc A))

Comm-full-abstraction : (p q : P A) → (p ≈ q) ⟷ (⟦ p ⟧ ≡ ⟦ q ⟧ᶜ)
Comm-full-abstraction p q .snd p≡q = Proc-full-abstraction p q .snd (sym (hom↓ p) ⨾ cong ⟦_⟧↓ p≡q ⨾ hom↓ q) 
Comm-full-abstraction p q .fst p≈q = sym (hom↑ p) ⨾ cong ⟦_⟧↑ (Proc-full-abstraction p q .fst p≈q) ⨾ hom↑ q