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

open import Algebra
open import Prelude hiding (P)

module CCS.Hyp.Renaming {r} {R : Type r} (mod : UnitalMagma R) where

open import CCS.Alg
open import CCS.SemiModel
open import CCS.Hyp.Definition
open import CCS.Hyp.Alg mod
open import Hyper.Base

open UnitalMagma mod

open ℍ-Alg

module _ {A : Type r} ⦃ _ : IsDiscrete A ⦄ where


  -- ν↑ n maps the name n to 𝕥, and everything else to 𝕚
  ν↑ : A → Communicator A R → Communicator (Maybe A) R
  ν↓ : A → Communicator (Maybe A) R → Communicator A R
  
  -- ν⇓ removes the 𝕥s
  ν⇓ : A → Communicator (Maybe A) R → Communicator A R
  ν⇑ : A → Communicator A R → Communicator (Maybe A) R
  
  ι (ν↑ n p) q m = ι p (ν↓ n q) (map-maybe (map-act (_?? n)) m)
  ι (ν↓ n p) q m = ι p (ν↑ n q) (map-maybe (map-act (λ m′ → guard (neg (does (n ≟ m′))) m′)) m)
  
  ι (ν⇑ n p) q 𝕥 = ι p (ν⇓ n q) 𝕥
  ι (ν⇑ n p) q (𝕚 τ) = ι p (ν⇓ n q) (𝕚 τ)
  ι (ν⇑ n p) q (𝕚 (inp (𝕚 m))) = ι p (ν⇓ n q) (𝕚 (inp m))
  ι (ν⇑ n p) q (𝕚 (inp 𝕥)) = ε
  ι (ν⇑ n p) q (𝕚 (out (𝕚 m))) = ι p (ν⇓ n q) (𝕚 (out m))
  ι (ν⇑ n p) q (𝕚 (out 𝕥)) = ε
  
  ι (ν⇓ n p) q 𝕥 = ι p (ν⇑ n q) 𝕥
  ι (ν⇓ n p) q (𝕚 m) = if does (n ∈ₐ? m) then ε else ι p (ν⇑ n q) (𝕚 (map-act 𝕚 m))
  
  ↓∘↑ : ∀ n p → ν↓ n (ν↑ n p) ≡ p
  ↓∘↑ n p = cong-ι (funExt ∘′ lemma n p)
    where
    lemma : ∀ n p h m → ι (ν↓ n (ν↑ n p)) h m ≡ ι p h m
    lemma n p h 𝕥 = cong (flip (ι p) 𝕥) (↓∘↑ n h)
    lemma n p h (𝕚 τ) = cong (flip (ι p) (𝕚 τ)) (↓∘↑ n h)
    lemma n p h (𝕚 (inp m)) with n ≟ m
    ... | yes n≡m = cong₂ (ι p) (↓∘↑ n h ) (cong (𝕚 ∘ inp) n≡m)
    ... | no  n≢m = cong (flip (ι p) (𝕚 (inp m))) (↓∘↑ n h)
    lemma n p h (𝕚 (out m)) with n ≟ m
    ... | yes n≡m = cong₂ (ι p) (↓∘↑ n h ) (cong (𝕚 ∘ out) n≡m)
    ... | no  n≢m = cong (flip (ι p) (𝕚 (out m))) (↓∘↑ n h)
  
  ν⇓∘ν↑ : ∀ n p → ν⇓ n (ν↑ n p) ≡ ν n - p
  ν↓∘ν⇑ : ∀ n p → ν↓ n (ν⇑ n p) ≡ ν n - p
  
  ν⇓∘ν↑ n p = cong-ι (funExt ∘′ lemma n p)
    where
    lemma :  (n : A) (p h : Communicator A R) (m : Maybe (Act A)) → ι (ν⇓ n (ν↑ n p)) h m ≡ ι (ν n - p) h m
    lemma n p h (𝕚 τ) i = ι p (ν↓∘ν⇑ n h i) (𝕚 τ)
    lemma n p h 𝕥 = cong (flip (ι p) 𝕥) (ν↓∘ν⇑ n h)
    lemma n p h (𝕚 (out m)) with n ≟ m
    ... | yes n≡m = refl
    ... | no n≢m = cong (flip (ι p) (𝕚 (out m))) (ν↓∘ν⇑ n h) 
    lemma n p h (𝕚 (inp m)) with n ≟ m
    ... | yes n≡m = refl
    ... | no n≢m = cong (flip (ι p) (𝕚 (inp m))) (ν↓∘ν⇑ n h) 
  
  ν↓∘ν⇑ n p = cong-ι (funExt ∘′ lemma n p)
    where
    lemma : ∀ n p h m → ι (ν↓ n (ν⇑ n p)) h m ≡ ι (ν n - p) h m
    lemma n p h (𝕚 τ) = cong (flip (ι p) (𝕚 τ)) (ν⇓∘ν↑ n h)
    lemma n p h 𝕥 = cong (flip (ι p) 𝕥) (ν⇓∘ν↑ n h)
    lemma n p h (𝕚 (out m)) with n ≟ m
    ... | yes n≡m = refl
    ... | no n≢m = cong (flip (ι p) (𝕚 (out m))) (ν⇓∘ν↑ n h)
    lemma n p h (𝕚 (inp m)) with n ≟ m
    ... | yes n≡m = refl
    ... | no n≢m = cong (flip (ι p) (𝕚 (inp m))) (ν⇓∘ν↑ n h)

ρ : (A ⟷ B) → Communicator A R → Communicator B R
ι (ρ f p) q m = ι p (ρ (swap f) q) (map-maybe (map-act (f .snd)) m)

ρ-⊕ : ∀ (f : A ⟷ B) p q → ρ f (p ℍ-Alg.⊕ q) ≡ ρ f p ℍ-Alg.⊕ ρ f q
ρ-⊕ f p q = cong-ι (λ _ → refl)

ρ-𝟘 : ∀ (f : A ⟷ B) → ρ f 𝟘 ≡ 𝟘
ρ-𝟘 f = cong-ι (λ _ → refl)

ρ⁻¹ : ∀ (f : A ⟷ B) → IsSection f → ∀ p → ρ f (ρ (swap f) p) ≡ p
ρ⁻¹ f isf p = cong-ι (funExt ∘′ lemma f isf p)
  where
  lemma : ∀ (f : A ⟷ B) → IsSection f → ∀ p h m → ι (ρ f (ρ (swap f) p)) h m ≡ ι p h m
  lemma f isf p h 𝕥 = cong (flip (ι p) 𝕥) (ρ⁻¹ f isf h)
  lemma f isf p h (𝕚 τ) = cong (flip (ι p) (𝕚 τ)) (ρ⁻¹ f isf h)
  lemma f isf p h (𝕚 (inp m)) = cong₂ (ι p) (ρ⁻¹ f isf h) (cong (𝕚 ∘ inp) (isf m))
  lemma f isf p h (𝕚 (out m)) = cong₂ (ι p) (ρ⁻¹ f isf h) (cong (𝕚 ∘ out) (isf m))

ρ-⌊ : ∀ (f : A ⇔ B) p q → ρ (bic f) (p ℍ-Alg.⌊ q) ≡ ρ (bic f) p ℍ-Alg.⌊ ρ (bic f) q
ρ-∥ : ∀ (f : A ⇔ B) p q → ρ (bic f) (p ℍ-Alg.∥ q) ≡ ρ (bic f) p ℍ-Alg.∥ ρ (bic f) q

ρ-∥ f′ p q =
  let f = bic f′
  in
  ρ f (p ∥ q) ≡⟨⟩
  ρ f (p ⌊ q ⊕ q ⌊ p) ≡⟨ ρ-⊕ f (p ⌊ q) (q ⌊ p) ⟩
  ρ f (p ⌊ q) ⊕ ρ f (q ⌊ p) ≡⟨ cong₂ _⊕_ (ρ-⌊ f′ p q) (ρ-⌊ f′ q p) ⟩
  ρ f p ⌊ ρ f q ⊕ ρ f q ⌊ ρ f p ≡⟨⟩
  ρ f p ∥ ρ f q ∎

ρ-⌊ f p q = cong-ι (λ h → funExt λ m → cong (flip (ι p) _) (lemma f p q h ))
  where
  lemma : ∀ f → ∀ p q h → q ∥ ρ (swap (bic f)) h ≡ ρ (swap (bic f)) (ρ (bic f) q ∥ h)
  lemma f′ p q h =
    let f = bic f′
    in
    q ∥ ρ (swap f) h ≡˘⟨ cong (_∥ _) (ρ⁻¹ (swap f) (leftInv f′) q) ⟩
    ρ (swap f) (ρ f q) ∥ ρ (swap f) h ≡˘⟨ ρ-∥ (sym-⇔ f′) (ρ f q) h ⟩
    ρ (swap f) (ρ f q ∥ h) ∎

ρ-id : (p : Communicator A R) → ρ (id , id) p ≡ p
ρ-id p = cong-ι λ q → funExt λ r → cong₂ (ι p) (ρ-id q) (lemma r)
  where
  lemma : ∀ r → map-maybe (map-act id) r ≡ r
  lemma (𝕚 (inp x)) = refl
  lemma (𝕚 (out x)) = refl
  lemma (𝕚 τ) = refl
  lemma 𝕥 = refl

ρ-∘ : ∀ (f : B ⟷ C) (g : A ⟷ B) p → ρ f (ρ g p) ≡ ρ (⟷-∘ f g) p
ρ-∘ f g p = cong-ι (funExt ∘′ lemma f g p)
  where
  lemma : ∀ (f : B ⟷ C) (g : A ⟷ B) p h m → ι (ρ f (ρ g p)) h m ≡ ι (ρ (⟷-∘ f g) p) h m
  lemma f g p h 𝕥        = cong₂ (ι p) (ρ-∘ (swap g) (swap f) h) refl
  lemma f g p h (𝕚 τ)       = cong₂ (ι p) (ρ-∘ (swap g) (swap f) h) refl
  lemma f g p h (𝕚 (inp m)) = cong₂ (ι p) (ρ-∘ (swap g) (swap f) h) refl
  lemma f g p h (𝕚 (out m)) = cong₂ (ι p) (ρ-∘ (swap g) (swap f) h) refl

ν-ρ-comm : ∀  ⦃ _ : IsDiscrete A ⦄ ⦃ _ : IsDiscrete B ⦄
           n (f : A ⇔ B) p
         → ν n - ρ (bic f) p ≡ ρ (bic f) (ν (f .inv n) - p)
ν-ρ-comm′ : ∀ ⦃ _ : IsDiscrete A ⦄ ⦃ _ : IsDiscrete B ⦄
              n (f : A ⇔ B) p h m
          → ι (ν n - ρ (bic f) p) h m ≡ ι (ρ (bic f) (ν (f .inv n) - p)) h m

ν-ρ-comm″ : ∀ ⦃ _ : IsDiscrete A ⦄ ⦃ _ : IsDiscrete B ⦄
              n (f : A ⇔ B) p
          → ν f .fun n - ρ (bic f) p ≡ ρ (bic f) (ν n - p)
ν-ρ-comm″ n f p = ν-ρ-comm (f .fun n) f p ⨾ cong (λ e → ρ (bic f) (ν e - p)) (leftInv f n)

ν-ρ-comm′ n f p h 𝕥        = cong₂ (ι p) (sym (ν-ρ-comm″ n (sym-⇔ f) h)) refl
ν-ρ-comm′ n f p h (𝕚 τ)       = cong₂ (ι p) (sym (ν-ρ-comm″ n (sym-⇔ f) h)) refl
ν-ρ-comm′ n f p h (𝕚 (out m)) with n ≟ m | f .inv n ≟ f .inv m
... | no n≢m | yes in≡im = absurd (n≢m (iso⇒inj (sym-⇔ f) .snd in≡im))
... | yes n≡m | no in≢im = absurd (in≢im (cong (f .inv) n≡m))
... | yes nm | yes inm = refl
... | no nm | no inm = cong₂ (ι p) (sym (ν-ρ-comm″ n (sym-⇔ f) h)) refl
ν-ρ-comm′ n f p h (𝕚 (inp m)) with n ≟ m | f .inv n ≟ f .inv m
... | no n≢m | yes in≡im = absurd (n≢m (iso⇒inj (sym-⇔ f) .snd in≡im))
... | yes n≡m | no in≢im = absurd (in≢im (cong (f .inv) n≡m))
... | yes nm | yes inm = refl
... | no nm | no inm = cong₂ (ι p) (sym (ν-ρ-comm″ n (sym-⇔ f) h)) refl

ν-ρ-comm n f p = cong-ι (funExt ∘′ ν-ρ-comm′ n f p)

module _ {A : Type r} ⦃ _ : IsDiscrete A ⦄ where
  open import Swaps {A = A}

  ν-ρ-wrap : ∀ (n m : A) (p : Communicator A R) →
             ν n - p ≡ ρ (n /͍ m) (ν m - ρ (m /͍ n) p)
  ν-ρ-wrap n m p =
    ν n - p ≡˘⟨ cong (ν n -_) (ρ-id p) ⟩
    ν n - ρ (id , id) p ≡˘⟨ cong₂ (λ f g → ν n - ρ (f , g) p) (funExt (swap-inv n m)) (funExt (swap-inv n m)) ⟩
    ν n - ρ (⟷-∘ (n /͍ m) (m /͍ n)) p ≡˘⟨ cong (ν n -_) (ρ-∘ _ _ p) ⟩
    ν n - ρ (n /͍ m) (ρ (m /͍ n) p) ≡⟨ ν-ρ-comm n (n /⇔ m) (ρ (m /͍ n) p) ⟩
    ρ (n /͍ m) (ν (fst (m /͍ n) n) - ρ (m /͍ n) p) ≡⟨ cong (λ e → ρ (n /͍ m) (ν e - ρ (m /͍ n) p)) (swap-req m n) ⟩
    ρ (n /͍ m) (ν m - ρ (m /͍ n) p) ∎