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

open import Prelude hiding (P; A)

module CCS.Homomorphism.PtoC where

open import Data.Nat

private
  A : Type
  A = ℕ

open import CCS.Alg
open import CCS.SemiModel
import CCS.Proc as ℙ
open import Algebra

open ℙ using (Proc; procAlg; procMod; cong-proc; isSetProc; ↯)

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.Fresh.Hyp

import CCS.Fresh.Proc as ℙ

open import CCS.Fresh
open import Swaps {A = A}

⟦_⟧↑ : Proc A → Communicator
⟦_⟧↑ = 𝒦⟦ alg ⟧ ∘ ↯
  where
  alg : Ψ[ xs ⦂ 𝒦 (Act A × Proc A) ] ↦ Communicator
  alg .fst ∅ = 𝟘
  alg .fst ⟅ a , x ⟆ = a · ⟦ x ⟧↑
  alg .fst (_ ⟨ xs ⟩∪ _ ⟨ ys ⟩) = xs ⊕ ys

  alg .snd .c-trunc _ = isSet-Communicator isSetProc
  alg .snd .c-comm _ p _ q = ⊕-comm p q
  alg .snd .c-idem _ p = ⊕-idem p
  alg .snd .c-ident _ p = 𝟘⊕ p
  alg .snd .c-assoc _ p _ q _ r = ⊕-assoc p q r

⟦_⟧ₚ : P A → Proc A
⟦_⟧ₚ = ⟦_⟧

⌊-hom↑    : (n : List A) (p q : P A) → ⟦ νₛ n - ⟦ p ⌊ q ⟧ₚ ⟧↑ ≡ νₛ n - ⟦ p ⌊ q ⟧ᶜ
∥-hom↑    : (n : List A) (p q : P A) → ⟦ νₛ n - ⟦ p ∥ q ⟧ₚ ⟧↑ ≡ νₛ n - ⟦ p ∥ q ⟧ᶜ
sync-hom↑ : ∀ (n : List A) (a : Act A) (p q : P A) → ⟦ νₛ n - ℙ.syncᵢₒ ⟦ a · p ⟧ₚ ⟦ q ⟧ₚ ⟧↑ ≡ νₛ n - syncᵢₒ ⟦ a · p ⟧ᶜ ⟦ q ⟧ᶜ
step-hom↑ : ∀ (n : List A) (a : Act A) (p q : P A) → ⟦ νₛ n - ℙ.stepₗ  ⟦ a · p ⟧ₚ ⟦ q ⟧ₚ ⟧↑ ≡ νₛ n - stepₗ  ⟦ a · p ⟧ᶜ ⟦ q ⟧ᶜ

∥-hom↑ n p q =
  ⟦ νₛ n - ⟦ p ∥ q ⟧ₚ ⟧↑ ≡⟨ cong ⟦_⟧↑ (cong (νₛ n -_) (⌊-∥ ⟦ p ⟧ ⟦ q ⟧) ⨾ νₛ-⊕ n _ _) ⟩

  ⟦ νₛ n - ⟦ p ⌊ q ⟧ₚ ⟧↑ ⊕ ⟦ νₛ n - ⟦ q ⌊ p ⟧ₚ ⟧↑ ≡⟨ cong₂ _⊕_ (⌊-hom↑ n p q) (⌊-hom↑ n q p) ⟩

  (νₛ n - ⟦ p ⌊ q ⟧ᶜ) ⊕ (νₛ n - ⟦ q ⌊ p ⟧ᶜ) ≡˘⟨ cong (νₛ n -_) (⌊-∥ ⟦ p ⟧ ⟦ q ⟧) ⨾ νₛ-⊕ n _ _ ⟩

  νₛ n - ⟦ p ∥ q ⟧ᶜ ∎

step-hom↑ n a p q with n ₛ∈ₐ? a
... | yes n∈a =
  ⟦ νₛ n - ℙ.stepₗ ⟦ a · p ⟧ₚ ⟦ q ⟧ₚ ⟧↑ ≡⟨ cong (⟦_⟧↑ ∘ νₛ n -_) (ℙ.step-is-step a ⟦ p ⟧ ⟦ q ⟧) ⟩
  ⟦ νₛ n - a · ⟦ p ∥ q ⟧ₚ ⟧↑ ≡⟨ cong ⟦_⟧↑ (νₛ-∈-· n a ⟦ p ∥ q ⟧ n∈a) ⟩
  ⟦ 𝟘 ⟧↑ ≡˘⟨ νₛ-∈-· n a ⟦ q ∥ p ⟧ n∈a ⟩
  νₛ n - a · ⟦ q ∥ p ⟧ᶜ ≡˘⟨ cong (νₛ n -_) (step-· a ⟦ p ⟧ ⟦ q ⟧) ⟩
  νₛ n - stepₗ ⟦ a · p ⟧ᶜ ⟦ q ⟧ᶜ ∎
... | no  n∉a =
  ⟦ νₛ n - ℙ.stepₗ ⟦ a · p ⟧ₚ ⟦ q ⟧ₚ ⟧↑ ≡⟨ cong (⟦_⟧↑ ∘ νₛ n -_) (ℙ.step-is-step a ⟦ p ⟧ ⟦ q ⟧) ⟩
  ⟦ νₛ n - a · ⟦ p ∥ q ⟧ₚ ⟧↑ ≡⟨ cong ⟦_⟧↑ (νₛ-∉-· n a ⟦ p ∥ q ⟧ n∉a) ⟩
  a · ⟦ νₛ n - ⟦ p ∥ q ⟧ₚ ⟧↑ ≡⟨ cong (a ·_) (∥-hom↑ n p q) ⟩
  a · νₛ n - ⟦ p ∥ q ⟧ᶜ ≡˘⟨ νₛ-∉-· n a ⟦ p ∥ q ⟧ n∉a ⟩
  νₛ n - a · ⟦ p ∥ q ⟧ᶜ ≡⟨ cong ((νₛ n -_) ∘ (a ·_)) (∥-comm ⟦ p ⟧ ⟦ q ⟧) ⟩
  νₛ n - a · ⟦ q ∥ p ⟧ᶜ ≡˘⟨ cong (νₛ n -_) (step-· a ⟦ p ⟧ ⟦ q ⟧) ⟩
  νₛ n - stepₗ ⟦ a · p ⟧ᶜ ⟦ q ⟧ᶜ ∎


sync-hom↑ n a p `𝟘 = cong ⟦_⟧↑ (cong (νₛ n -_) (ℙ.sync𝟘ʳ ⟦ a · p ⟧) ⨾ νₛ-𝟘 n) ⨾ sym (νₛ-𝟘 n) ⨾ cong (νₛ n -_) (sym (sync𝟘ʳ a p))

sync-hom↑ n a p (q `⊕ r) =
  ⟦ νₛ n - ℙ.syncᵢₒ ⟦ a · p ⟧ₚ ⟦ q ⊕ r ⟧ₚ ⟧↑

    ≡⟨ cong ⟦_⟧↑ (cong (νₛ n -_) (ℙ.syncᵢₒ-⊕ʳ _ ⟦ q ⟧ ⟦ r ⟧) ⨾ νₛ-⊕ n _ _) ⟩

  ⟦ νₛ n - ℙ.syncᵢₒ ⟦ a · p ⟧ₚ ⟦ q ⟧ₚ ⟧↑ ⊕ ⟦ νₛ n - ℙ.syncᵢₒ ⟦ a · p ⟧ₚ ⟦ r ⟧ₚ ⟧↑

    ≡⟨ cong₂ _⊕_ (sync-hom↑ n a p q) (sync-hom↑ n a p r) ⟩

  (νₛ n - syncᵢₒ ⟦ a · p ⟧ᶜ ⟦ q ⟧ᶜ) ⊕ (νₛ n - syncᵢₒ ⟦ a · p ⟧ᶜ ⟦ r ⟧ᶜ)

    ≡˘⟨ cong (νₛ n -_) (syncᵢₒ-⊕ʳ a _ _ _) ⨾ νₛ-⊕ n _ _ ⟩

  νₛ n - syncᵢₒ ⟦ a · p ⟧ᶜ ⟦ q ⊕ r ⟧ᶜ ∎

sync-hom↑ n a p (q `⌊ r) =

  ⟦ νₛ n - ℙ.syncᵢₒ ⟦ a · p ⟧ₚ ⟦ q ⌊ r ⟧ₚ ⟧↑

    ≡˘⟨ cong (⟦_⟧↑ ∘ (νₛ n -_)) (ℙ.syncᵢₒ-assoc a ⟦ p ⟧ ⟦ r ⟧ ⟦ q ⟧) ⟩

  ⟦ νₛ n - ℙ.syncᵢₒ ⟦ a · (p ∥ r) ⟧ₚ ⟦ q ⟧ₚ ⟧↑

    ≡⟨ sync-hom↑ n a (p ∥ r) q ⟩

  νₛ n - syncᵢₒ ⟦ a · (p ∥ r) ⟧ᶜ ⟦ q ⟧ᶜ

    ≡˘⟨ cong (νₛ n -_) ( syncᵢₒ-assoc a ⟦ p ⟧ ⟦ q ⟧ ⟦ r ⟧) ⟩

  νₛ n - syncᵢₒ ⟦ a · p ⟧ᶜ ⟦ q ⌊ r ⟧ᶜ ∎

sync-hom↑ n a p (q `∥ r) =

  ⟦ νₛ n - ℙ.syncᵢₒ ⟦ a · p ⟧ₚ ⟦ q ∥ r ⟧ₚ ⟧↑

    ≡⟨ cong ⟦_⟧↑ (cong (νₛ n -_) (cong (ℙ.syncᵢₒ ⟦ a · p ⟧ₚ) (cong-proc refl) ⨾ ℙ.syncᵢₒ-⊕ʳ ⟦ a · p ⟧ ⟦ q ⌊ r ⟧ ⟦ r ⌊ q ⟧) ⨾ νₛ-⊕ n _ _) ⟩

  ⟦ νₛ n - ℙ.syncᵢₒ ⟦ a · p ⟧ₚ ⟦ q ⌊ r ⟧ₚ ⟧↑ ⊕ ⟦ νₛ n - ℙ.syncᵢₒ ⟦ a · p ⟧ₚ ⟦ r ⌊ q ⟧ₚ ⟧↑

    ≡⟨ cong₂ _⊕_ (sync-hom↑ n a p (q ⌊ r)) (sync-hom↑ n a p (r ⌊ q)) ⟩

  (νₛ n - syncᵢₒ ⟦ a · p ⟧ᶜ ⟦ q ⌊ r ⟧ᶜ) ⊕ (νₛ n - syncᵢₒ ⟦ a · p ⟧ᶜ ⟦ r ⌊ q ⟧ᶜ)

    ≡˘⟨ cong (νₛ n -_) (syncᵢₒ-⊕ʳ a ⟦ p ⟧ ⟦ q ⌊ r ⟧ ⟦ r ⌊ q ⟧) ⨾ νₛ-⊕ n _ _ ⟩

  νₛ n - syncᵢₒ ⟦ a · p ⟧ᶜ ⟦ q ∥ r ⟧ᶜ ∎

sync-hom↑ n a p (`! q) =

  ⟦ νₛ n - ℙ.syncᵢₒ ( a · ⟦ p ⟧ₚ) ⟦ ! q ⟧ₚ ⟧↑

    ≡⟨ cong ⟦_⟧↑ (cong (νₛ n -_) (cong (ℙ.syncᵢₒ (a · ⟦ p ⟧ₚ)) (!-⌊ ⟦ q ⟧ₚ) ⨾ sym (ℙ.syncᵢₒ-assoc a ⟦ p ⟧ₚ ⟦ ! q ⟧ₚ ⟦ q ⟧ₚ) )) ⟩

  ⟦ νₛ n - ℙ.syncᵢₒ (a · (⟦ p ⟧ₚ ∥ ⟦ ! q ⟧ₚ)) ⟦ q ⟧ₚ ⟧↑

    ≡⟨⟩

  ⟦ νₛ n - ℙ.syncᵢₒ (a · ⟦ p ∥ ! q ⟧ₚ) ⟦ q ⟧ₚ ⟧↑

    ≡⟨ sync-hom↑ n a (p ∥ ! q) q ⟩

  νₛ n - syncᵢₒ ⟦ a · (p ∥ ! q) ⟧ᶜ ⟦ q ⟧ᶜ

    ≡˘⟨ cong (νₛ n -_) (syncᵢₒ-assoc a ⟦ p ⟧ ⟦ q ⟧ ⟦ ! q ⟧) ⟩

  νₛ n - syncᵢₒ ⟦ a · p ⟧ᶜ ⟦ q ⌊ ! q ⟧ᶜ 

    ≡˘⟨ cong ((νₛ n -_) ∘ syncᵢₒ ⟦ a · p ⟧ᶜ ) (!-⌊ ⟦ q ⟧ᶜ) ⟩

  νₛ n - syncᵢₒ ⟦ a · p ⟧ᶜ ⟦ ! q ⟧ᶜ ∎

sync-hom↑ ns a p (`ν n - q) =

  let m = # ((a · p) ⌊ q)
      m∉ = #-∉ ((a · p) ⌊ q)
  in

  ⟦ νₛ ns - ℙ.syncᵢₒ (a · ⟦ p ⟧ₚ) ⟦ ν n - q ⟧ₚ ⟧↑

    ≡⟨ cong ⟦_⟧↑ (cong (νₛ ns -_) (ℙ.ν-sync-rewrite n a p q)) ⟩

  ⟦ νₛ (m ∷ ns) - ℙ.syncᵢₒ (a · ⟦ p ⟧ₚ) ⟦ `ρ (n /→ m) q ⟧ₚ ⟧↑

    ≡⟨ sync-hom↑ (m ∷ ns) a p (`ρ (n /→ m) q) ⟩

  νₛ (m ∷ ns) - syncᵢₒ (a · ⟦ p ⟧ᶜ) ⟦ `ρ (n /→ m) q ⟧ᶜ

    ≡˘⟨ ν-sync-rewrite ns n a p q ⟩

  νₛ ns - syncᵢₒ ⟦ a · p ⟧ᶜ ⟦ ν n - q ⟧ᶜ ∎

sync-hom↑ n τ p q = cong ⟦_⟧↑ (cong (νₛ n -_) (cong-proc refl) ⨾ νₛ-𝟘 n) ⨾ sym (cong (νₛ n -_) (sync-τ ⟦ p ⟧ q) ⨾  νₛ-𝟘 n)
sync-hom↑ n (out a) p q = cong ⟦_⟧↑ (cong (νₛ n -_) (cong-proc refl) ⨾ νₛ-𝟘 n) ⨾ sym (cong (νₛ n -_) (sync-out a ⟦ p ⟧ q) ⨾ νₛ-𝟘 n)

sync-hom↑ n (inp a) p (inp b `· q) = cong ⟦_⟧↑ (cong (νₛ n -_) (cong-proc refl) ⨾ νₛ-𝟘 n) ⨾ sym (cong (νₛ n -_) (sync-nomatch (inp a) (inp b) ⟦ p ⟧ ⟦ q ⟧ λ ()) ⨾  νₛ-𝟘 n)
sync-hom↑ n (inp a) p (τ `· q) = cong ⟦_⟧↑ (cong (νₛ n -_) (cong-proc refl) ⨾ νₛ-𝟘 n) ⨾ sym (cong (νₛ n -_) (sync-nomatch (inp a) τ ⟦ p ⟧ ⟦ q ⟧ λ ()) ⨾  νₛ-𝟘 n)

sync-hom↑ n (inp a) p (out b `· q) with a ≟ b
... | yes a≡b =

  ⟦ νₛ n - ℙ.syncᵢₒ (inp a · ⟦ p ⟧ₚ) (out b · ⟦ q ⟧ₚ) ⟧↑

    ≡⟨ cong (⟦_⟧↑ ∘ νₛ n -_) (cong-proc (cong (bool _ _) (it-does (a ≟ b) a≡b))) ⟩

  ⟦ νₛ n - τ · ⟦ p ∥ q ⟧ₚ ⟧↑

    ≡⟨ cong ⟦_⟧↑ (νₛ-∉-· n τ ⟦ p ∥ q ⟧ₚ (λ ())) ⟩

  ⟦ τ · νₛ n - ⟦ p ∥ q ⟧ₚ ⟧↑

    ≡⟨ cong (τ ·_) (∥-hom↑ n p q) ⟩

  τ · νₛ n - ⟦ p ∥ q ⟧ᶜ

    ≡˘⟨  νₛ-∉-· n τ ⟦ p ∥ q ⟧ᶜ (λ ()) ⟩

  νₛ n - τ · ⟦ p ∥ q ⟧ᶜ

    ≡˘⟨ cong (νₛ n -_) (sync-match (inp a) (out b) p ⟦ q ⟧ᶜ a≡b ) ⟩

  νₛ n - syncᵢₒ (inp a · ⟦ p ⟧ᶜ) (out b · ⟦ q ⟧ᶜ) ∎

... | no a≢b =

  ⟦ νₛ n - ℙ.syncᵢₒ (inp a · ⟦ p ⟧ₚ) (out b · ⟦ q ⟧ₚ) ⟧↑

    ≡⟨ cong (⟦_⟧↑ ∘ νₛ n -_) (cong-proc (cong (bool _ _) (it-doesn't (a ≟ b) a≢b))) ⟩

  ⟦ νₛ n - 𝟘 ⟧↑

    ≡⟨ cong ⟦_⟧↑ (νₛ-𝟘 n) ⟩

  ⟦ 𝟘 ⟧↑

    ≡⟨⟩

  𝟘

    ≡˘⟨ νₛ-𝟘 n ⟩

  νₛ n - 𝟘

    ≡˘⟨ cong (νₛ n -_) (sync-nomatch (inp a) (out b) ⟦ p ⟧ᶜ ⟦ q ⟧ᶜ a≢b ) ⟩

  νₛ n - syncᵢₒ (inp a · ⟦ p ⟧ᶜ) (out b · ⟦ q ⟧ᶜ) ∎

⌊-hom↑ n `𝟘 q = cong ⟦_⟧↑ (ν⌊-𝟘 n ⟦ q ⟧) ⨾ sym (ν⌊-𝟘 n ⟦ q ⟧)
⌊-hom↑ n (p `⊕ q) r =
  ⟦ νₛ n - ⟦ (p ⊕ q) ⌊ r ⟧ ⟧↑ ≡⟨ cong ⟦_⟧↑ (ν⌊-⊕ ⟦ p ⟧ ⟦ q ⟧ n ⟦ r ⟧) ⟩
  ⟦ νₛ n - ⟦ p ⌊ r ⟧ ⟧↑ ⊕ ⟦ νₛ n - ⟦ q ⌊ r ⟧ ⟧↑ ≡⟨ cong₂ _⊕_ (⌊-hom↑ n p r) (⌊-hom↑ n q r) ⟩
  νₛ n - ⟦ p ⌊ r ⟧ ⊕ νₛ n - ⟦ q ⌊ r ⟧ ≡˘⟨ ν⌊-⊕ ⟦ p ⟧ ⟦ q ⟧ n ⟦ r ⟧ ⟩
  νₛ n - ⟦ (p ⊕ q) ⌊ r ⟧ ∎
⌊-hom↑ n (p `⌊ q) r =
  ⟦ νₛ n - ⟦ (p ⌊ q) ⌊ r ⟧ ⟧↑ ≡⟨ cong (λ e → ⟦ νₛ n - e ⟧↑) (⌊-assoc _ _ _) ⟩
  ⟦ νₛ n - ⟦ p ⌊ (q ∥ r) ⟧ ⟧↑ ≡⟨ ⌊-hom↑ n p (q ∥ r) ⟩
  νₛ n - ⟦ p ⌊ (q ∥ r) ⟧ ≡˘⟨ cong (νₛ n -_) (⌊-assoc _ _ _ ) ⟩
  νₛ n - ⟦ (p ⌊ q) ⌊ r ⟧ ∎
⌊-hom↑ n (a `· p) q =
  ⟦ νₛ n - ⟦ (a · p) ⌊ q ⟧ ⟧↑ ≡⟨⟩
  ⟦ νₛ n - (⟦ a · p ⟧ ⌊ ⟦ q ⟧) ⟧↑ ≡⟨ cong (λ e → ⟦ νₛ n - e ⟧↑) (ℙ.step-sync _ _) ⟩
  ⟦ νₛ n - (ℙ.syncᵢₒ ⟦ a · p ⟧ ⟦ q ⟧ ⊕ ℙ.stepₗ ⟦ a · p ⟧ ⟦ q ⟧) ⟧↑ ≡⟨ cong ⟦_⟧↑ (νₛ-⊕ n _ _) ⟩
  ⟦ νₛ n - ℙ.syncᵢₒ ⟦ a · p ⟧ ⟦ q ⟧ ⟧↑ ⊕ ⟦ νₛ n - ℙ.stepₗ ⟦ a · p ⟧ ⟦ q ⟧ ⟧↑ ≡⟨ cong₂ _⊕_ (sync-hom↑ n a p q) (step-hom↑ n a p q) ⟩
  (νₛ n - syncᵢₒ ⟦ a · p ⟧ ⟦ q ⟧) ⊕ (νₛ n - stepₗ ⟦ a · p ⟧ ⟦ q ⟧) ≡˘⟨ νₛ-⊕ n _ _  ⟩
  νₛ n - (syncᵢₒ (a · ⟦ p ⟧) ⟦ q ⟧ ⊕ stepₗ (a · ⟦ p ⟧) ⟦ q ⟧) ≡˘⟨ cong (νₛ n -_) (·⌊-decomp a ⟦ p ⟧ ⟦ q ⟧) ⟩
  νₛ n - (a · ⟦ p ⟧ ⌊ ⟦ q ⟧) ≡⟨⟩
  νₛ n - ⟦ (a · p) ⌊ q ⟧ ∎

⌊-hom↑ n (p `∥ q) r = 
  ⟦ νₛ n - ⟦ (p ∥ q) ⌊ r ⟧ ⟧↑ ≡⟨ cong (⟦_⟧↑ ∘ (νₛ n -_)) (cong-proc refl) ⟩
  ⟦ νₛ n - ⟦ (p ⌊ q ⊕ q ⌊ p) ⌊ r ⟧ ⟧↑ ≡⟨ cong (⟦_⟧↑ ∘ νₛ n -_) (⊕⌊ ⟦ p ⌊ q ⟧ ⟦ q ⌊ p ⟧ _) ⟩
  ⟦ νₛ n - ⟦ (p ⌊ q) ⌊ r ⊕ (q ⌊ p) ⌊ r ⟧ ⟧↑ ≡⟨ cong ⟦_⟧↑ (νₛ-⊕ n _ _) ⟩
  ⟦ νₛ n - ⟦ (p ⌊ q) ⌊ r ⟧ ⟧↑ ⊕ ⟦ νₛ n - ⟦ (q ⌊ p) ⌊ r ⟧ ⟧↑ ≡⟨ cong₂ _⊕_ (⌊-hom↑ n (p ⌊ q) r) (⌊-hom↑ n (q ⌊ p) r) ⟩
  (νₛ n - ⟦ (p ⌊ q) ⌊ r ⟧) ⊕ (νₛ n - ⟦ (q ⌊ p) ⌊ r ⟧) ≡˘⟨ νₛ-⊕ n _ _ ⟩
  νₛ n - ⟦ (p ⌊ q) ⌊ r ⊕ (q ⌊ p) ⌊ r ⟧ ≡˘⟨ cong (νₛ n -_) (⊕⌊ ⟦ p ⌊ q ⟧ ⟦ q ⌊ p ⟧ _) ⟩
  νₛ n - ⟦ (p ⌊ q ⊕ q ⌊ p) ⌊ r ⟧ ≡˘⟨ cong (νₛ n -_) (cong (_⌊ ⟦ r ⟧) (⌊-∥ ⟦ p ⟧ ⟦ q ⟧)) ⟩
  νₛ n - ⟦ (p ∥ q) ⌊ r ⟧ ∎

⌊-hom↑ n (`! p) q =
  ⟦ νₛ n - ⟦ ! p ⌊ q ⟧ ⟧↑ ≡⟨ cong (λ p′ → ⟦ νₛ n - (p′ ⌊ ⟦ q ⟧) ⟧↑) (!-⌊ ⟦ p ⟧) ⟩
  ⟦ νₛ n - ⟦ (p ⌊ ! p) ⌊ q ⟧ ⟧↑ ≡⟨ ⌊-hom↑ n (p ⌊ ! p) q  ⟩
  νₛ n - ⟦ (p ⌊ ! p) ⌊ q ⟧ ≡˘⟨ cong (λ p′ → νₛ n - (p′ ⌊ ⟦ q ⟧)) (!-⌊ ⟦ p ⟧) ⟩
  νₛ n - ⟦ ! p ⌊ q ⟧ ∎


⌊-hom↑ ns (`ν n - p) q =
  let m = # (p ⌊ q)
  in
  ⟦ νₛ ns - ⟦ ν n - p ⌊ q ⟧ ⟧↑ ≡⟨ cong ⟦_⟧↑ (ℙ.ν-⌊-rewrite ns n p q) ⟩
  ⟦ νₛ (m ∷ ns) - ⟦ `ρ (n /→ m) p ⌊ q ⟧ ⟧↑ ≡⟨ ⌊-hom↑ (m ∷ ns) (`ρ (n /→ m) p) q ⟩
  νₛ (m ∷ ns) - ⟦ `ρ (n /→ m) p ⌊ q ⟧ ≡˘⟨ ν-⌊-rewrite ns n p q ⟩
  νₛ ns - ⟦ ν n - p ⌊ q ⟧ ∎