{-# OPTIONS --safe --without-K #-}
 
--------------------------------------------------------------------------------
-- Wire-coherence theory: the ⟦_⟧ᵇ-free coherence of the structural
-- `wires`/`HomTerm` layer still consumed by the solver — the `castW`
-- object-transport algebra, the +-associators, and the flat-shift/merge-split
-- bridge `liftW-merge` (`WireCoh`), plus the DecEq-dependent UIP/castW-collapse
-- layer, the `castW-id⊗ˡ` helper, and the merge/split right-unitor & pentagon
-- coherence family `merge-ρ`/`split-ρ`/`merge-assoc`/`split-assoc`
-- (`WireCohDec`), which `Reflect.embed-resp-≈` and `Frontend.Core` consume.
--------------------------------------------------------------------------------
 
module Categories.Coherence.Monoidal.WireCoherence where
 
open import categorical-crypto.Prelude hiding (_∘_; id; map; merge)
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality.Properties
import Data.List.Properties.Ext as ListExt
 
open import Categories.Category
import Categories.Category.Monoidal.Properties as MonProps
import Categories.Category.Monoidal.Reasoning as MonR
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Reasoning.Ext as MRExt
open import Categories.FreeMonoidal
 
module WireCoh (v : Variant) (X : Set)
               (mor : FreeMonoidalHelper.ObjTerm v X → FreeMonoidalHelper.ObjTerm v X → Set)
               where
  open FreeMonoidalHelper v X
  open FreeMonoidalHelper.Mor v X mor
  open Category.HomReasoning FreeMonoidal
  open MonR Monoidal-FreeMonoidal using (refl⟩⊗⟨_; _⟩⊗⟨refl; _⟩⊗⟨_; split₁ʳ; serialize₁₂)
  open MR FreeMonoidal
  open MRExt FreeMonoidal
 
  -- the object transport along a propositional equality of wire-lists.
  castW : ∀ {u v : List X} → u ≡ v → HomTerm (wires u) (wires v)
  castW refl = id
 
  castW-∷ : ∀ {x : X} {u v : List X} (e : u ≡ v) → id ⊗₁ castW e ≈Term castW (cong (x ∷_) e)
  castW-∷ refl = id⊗id≈id
 
  castW-isoˡ : ∀ {u v : List X} (e : u ≡ v) → castW (sym e) ∘ castW e ≈Term id
  castW-isoˡ refl = idˡ
 
  castW-isoʳ : ∀ {u v : List X} (e : u ≡ v) → castW e ∘ castW (sym e) ≈Term id
  castW-isoʳ refl = idˡ
  --------------------------------------------------------------------------------
  -- The structural associators on wire-lists
  --------------------------------------------------------------------------------
  assocW : (p q s : List X) → HomTerm (wires (p ++ (q ++ s))) (wires ((p ++ q) ++ s))
  assocW p q s = castW (sym (++-assoc p q s))
 
  assocW⁻ : (p q s : List X) → HomTerm (wires ((p ++ q) ++ s)) (wires (p ++ (q ++ s)))
  assocW⁻ p q s = castW (++-assoc p q s)
 
  -- `assocW`/`assocW⁻` are mutually inverse (they are `castW` of `sym`-related indices).
  assocW⁻∘assocW : ∀ (p q s : List X) → assocW⁻ p q s ∘ assocW p q s ≈Term id
  assocW⁻∘assocW p q s = castW-isoʳ (++-assoc p q s)
  -- Flat-shift of a wire morphism as a merge/split conjugation.  `liftW p W`
  -- (the prefix-idle lift, `id {wires p} ⊗₁ W` reflattened) equals the box `W`
  -- conjugated by the flat `merge p`/`split p`; and the flat `pad` is literally
  -- the wire-shift of the right-pad `rpad`.  Both are ⟦_⟧ᵇ-free wire coherence.
 
  -- the flat shift equals the merge/split conjugation.
  liftW-merge : ∀ (p : List X) {u v} (W : HomTerm (wires u) (wires v))
              → liftW p W ≈Term merge p ∘ (id ⊗₁ W) ∘ split p
  liftW-merge []      W = introʳ λ⇒∘λ⇐≈id ○ pullˡ (⟺ λ⇒∘id⊗f≈f∘λ⇒) ○ assoc
  liftW-merge (x ∷ p) {u} {v} W =
    (refl⟩⊗⟨ liftW-merge p W)
      ○ (⟺ (id⊗-∘3 (merge p) (id ⊗₁ W) (split p)))
      ○ reassoc-suc
    where
      -- insert α⇒∘α⇐ = id in the middle and reassociate to expose
      -- merge (suc p) = id⊗₁merge p ∘ α⇒ and split (suc p) = α⇐ ∘ id⊗₁split p.
      reassoc-suc :
          id ⊗₁ merge p ∘ (id ⊗₁ (id ⊗₁ W) ∘ id ⊗₁ split p)
        ≈Term (id ⊗₁ merge p ∘ α⇒) ∘ id ⊗₁ W ∘ (α⇐ ∘ id ⊗₁ split p)
      reassoc-suc = begin
        id ⊗₁ merge p ∘ (id ⊗₁ (id ⊗₁ W) ∘ id ⊗₁ split p)
          ≈⟨ refl⟩∘⟨ insertInner α⇒∘α⇐≈id ⟩
        id ⊗₁ merge p ∘ ((id ⊗₁ (id ⊗₁ W) ∘ α⇒) ∘ (α⇐ ∘ id ⊗₁ split p))
          ≈⟨ refl⟩∘⟨ ((⟺ α-comm) ○ (refl⟩∘⟨ (id⊗id≈id ⟩⊗⟨refl))) ⟩∘⟨refl ⟩
        id ⊗₁ merge p ∘ ((α⇒ ∘ id ⊗₁ W) ∘ (α⇐ ∘ id ⊗₁ split p))
          ≈⟨ center ≈-Term-refl ⟨
        (id ⊗₁ merge p ∘ α⇒) ∘ id ⊗₁ W ∘ (α⇐ ∘ id ⊗₁ split p) ∎
 
  --------------------------------------------------------------------------------
  -- The DecEq-dependent layer: `castW` is determined by its
  -- endpoints. On top of that UIP fact this holds the castW helper
  -- kit, the merge/split right-unitor & pentagon coherence family,
  -- and the structural reassociators' collapse to `castW`.
  --------------------------------------------------------------------------------
  module WireCohDec ⦃ _ : DecEq X ⦄ where
    ≡-irrelevantL : ∀ {x y : List X} (e e' : x ≡ y) → e ≡ e'
    ≡-irrelevantL = ListExt.≡-irrelevant _≟_
 
    castW-irr : ∀ {u v : List X} (e e' : u ≡ v) → castW e ≈Term castW e'
    castW-irr e e' = ≡⇒≈Term (cong castW (≡-irrelevantL e e'))
 
    -- push a coercion along `cong (x ∷_)` under the prefix `id {Var x} ⊗₁ _`;
    -- the other end is an ARBITRARY object, since the merge/split steps below
    -- need bracketed tensors of wires, not flat ones.
    castW-id⊗ˡ : ∀ {R} (x : X) {p q : List X} (e : p ≡ q) (h : HomTerm R (wires p))
               → castW (cong (x ∷_) e) ∘ (id ⊗₁ h) ≈Term id ⊗₁ (castW e ∘ h)
    castW-id⊗ˡ x e h = (⟺ (castW-∷ e) ⟩∘⟨refl) ○ id⊗-∘ (castW e) h
 
    --------------------------------------------------------------------------------
    -- The merge/split coherence family: the right-unitor coherence on the flat
    -- merge/split (`merge-ρ`/`split-ρ`, ≈ ρ⇒/ρ⇐) and the pentagon associativity
    -- of merge/split (`merge-assoc`/`split-assoc`).  Pure ⟦_⟧ᵇ-free wire
    -- coherence — the merge/split analogue of the assocW/castW theory above.
    -- They bottom out in the Mac Lane / Kelly unit coherence laws at the *free*
    -- monoidal category over `mor`, whose _≈_/α⇒/ρ⇒/λ⇒/_⊗₁_ coincide
    -- DEFINITIONALLY with _≈Term_/α⇒/ρ⇒/λ⇒/_⊗₁_, so these land as `≈Term`.
    --------------------------------------------------------------------------------
    module K = MonProps.Kelly's Monoidal-FreeMonoidal
 
    merge-ρ : (a : List X) → castW (++-identityʳ a) ∘ merge a ≈Term ρ⇒
    merge-ρ []      = idˡ ○ K.coherence₃
    merge-ρ (x ∷ a) = begin
      castW (++-identityʳ (x ∷ a)) ∘ (id ⊗₁ merge a ∘ α⇒)
        ≈⟨ ⟺ assoc ⟩
      (castW (cong (x ∷_) (++-identityʳ a)) ∘ (id ⊗₁ merge a)) ∘ α⇒
        ≈⟨ (castW-id⊗ˡ x (++-identityʳ a) (merge a)) ⟩∘⟨refl ⟩
      id ⊗₁ (castW (++-identityʳ a) ∘ merge a) ∘ α⇒
        ≈⟨ (refl⟩⊗⟨ (merge-ρ a)) ⟩∘⟨refl ⟩
      id ⊗₁ ρ⇒ ∘ α⇒
        ≈⟨ K.coherence₂ ⟩
      ρ⇒ ∎
 
    split-ρ : (a : List X) → split a ∘ castW (sym (++-identityʳ a)) ≈Term ρ⇐
    split-ρ a = inv-resp fi-f ρ⇒∘ρ⇐≈id (merge-ρ a)
      where
        e = ++-identityʳ a
        fi-f : (split a ∘ castW (sym e)) ∘ (castW e ∘ merge a) ≈Term id
        fi-f = cancelInner (castW-isoˡ e) ○ split∘merge a
 
    merge-assoc : ∀ (p q r : List X)
      → merge p ∘ (id ⊗₁ merge q) ∘ α⇒ ≈Term assocW⁻ p q r ∘ (merge (p ++ q) ∘ (merge p ⊗₁ id))
    merge-assoc []      q r = begin
      λ⇒ ∘ (id ⊗₁ merge q) ∘ α⇒
        ≈⟨ pullˡ λ⇒∘id⊗f≈f∘λ⇒ ⟩
      (merge q ∘ λ⇒) ∘ α⇒
        ≈⟨ pullʳ K.coherence₁ ⟩
      merge q ∘ (λ⇒ ⊗₁ id)
        ≈⟨ ⟺ idˡ ⟩
      assocW⁻ [] q r ∘ (merge q ∘ (λ⇒ ⊗₁ id)) ∎
    merge-assoc (x ∷ p) q r = begin
      (id ⊗₁ merge p ∘ α⇒) ∘ (id ⊗₁ merge q) ∘ α⇒
        ≈⟨ refl⟩∘⟨ (((⟺ id⊗id≈id) ⟩⊗⟨refl) ⟩∘⟨refl) ⟩
      (id ⊗₁ merge p ∘ α⇒) ∘ ((id ⊗₁ id) ⊗₁ merge q) ∘ α⇒
        ≈⟨ center α-comm ⟩
      id ⊗₁ merge p ∘ ((id ⊗₁ (id ⊗₁ merge q) ∘ α⇒) ∘ α⇒)
        ≈⟨ ⟺ assoc ⟩
      (id ⊗₁ merge p ∘ (id ⊗₁ (id ⊗₁ merge q) ∘ α⇒)) ∘ α⇒
        ≈⟨ (pullˡ (id⊗-∘ (merge p) (id ⊗₁ merge q))) ⟩∘⟨refl ⟩
      ((id ⊗₁ (merge p ∘ (id ⊗₁ merge q))) ∘ α⇒) ∘ α⇒
        ≈⟨ pent ⟩
      (id ⊗₁ (merge p ∘ (id ⊗₁ merge q)) ∘ id ⊗₁ α⇒) ∘ (α⇒ ∘ α⇒ ⊗₁ id)
        ≈⟨ (id⊗-∘ (merge p ∘ (id ⊗₁ merge q)) α⇒) ⟩∘⟨refl ⟩
      (id ⊗₁ ((merge p ∘ (id ⊗₁ merge q)) ∘ α⇒)) ∘ (α⇒ ∘ α⇒ ⊗₁ id)
        ≈⟨ (refl⟩⊗⟨ (assoc ○ (merge-assoc p q r))) ⟩∘⟨refl ⟩
      (id ⊗₁ (assocW⁻ p q r ∘ (merge (p ++ q) ∘ (merge p ⊗₁ id)))) ∘ (α⇒ ∘ α⇒ ⊗₁ id)
        ≈⟨ (⟺ (castW-id⊗ˡ x (++-assoc p q r) _)) ⟩∘⟨refl ⟩
      (assocW⁻ (x ∷ p) q r ∘ (id ⊗₁ (merge (p ++ q) ∘ (merge p ⊗₁ id)))) ∘ (α⇒ ∘ α⇒ ⊗₁ id)
        ≈⟨ assoc ⟩
      assocW⁻ (x ∷ p) q r ∘ ((id ⊗₁ (merge (p ++ q) ∘ (merge p ⊗₁ id))) ∘ (α⇒ ∘ α⇒ ⊗₁ id))
        ≈⟨ refl⟩∘⟨ tailRHS ⟩
      assocW⁻ (x ∷ p) q r ∘ (((id ⊗₁ merge (p ++ q)) ∘ α⇒) ∘ ((id ⊗₁ merge p ∘ α⇒) ⊗₁ id)) ∎
      where
        pent : ∀ {B} {X : HomTerm (Var x ⊗₀ (wires p ⊗₀ (wires q ⊗₀ wires r))) B}
             → (X ∘ α⇒) ∘ α⇒ ≈Term (X ∘ id ⊗₁ α⇒) ∘ (α⇒ ∘ α⇒ ⊗₁ id)
        pent = pullʳ (⟺ pentagon) ○ ⟺ assoc
 
        tailRHS : (id ⊗₁ (merge (p ++ q) ∘ (merge p ⊗₁ id))) ∘ (α⇒ ∘ α⇒ ⊗₁ id)
                ≈Term ((id ⊗₁ merge (p ++ q)) ∘ α⇒) ∘ ((id ⊗₁ merge p ∘ α⇒) ⊗₁ id)
        tailRHS = begin
          (id ⊗₁ (merge (p ++ q) ∘ (merge p ⊗₁ id))) ∘ (α⇒ ∘ α⇒ ⊗₁ id)
            ≈⟨ (⟺ (id⊗-∘ (merge (p ++ q)) (merge p ⊗₁ id))) ⟩∘⟨refl ⟩
          (id ⊗₁ merge (p ++ q) ∘ id ⊗₁ (merge p ⊗₁ id)) ∘ (α⇒ ∘ α⇒ ⊗₁ id)
            ≈⟨ center (⟺ α-comm) ⟩
          id ⊗₁ merge (p ++ q) ∘ ((α⇒ ∘ (id ⊗₁ merge p) ⊗₁ id) ∘ α⇒ ⊗₁ id)
            ≈⟨ refl⟩∘⟨ pullʳ (⟺ split₁ʳ) ⟩
          id ⊗₁ merge (p ++ q) ∘ (α⇒ ∘ ((id ⊗₁ merge p ∘ α⇒) ⊗₁ id))
            ≈⟨ ⟺ assoc ⟩
          (id ⊗₁ merge (p ++ q) ∘ α⇒) ∘ ((id ⊗₁ merge p ∘ α⇒) ⊗₁ id) ∎
 
    split-assoc : ∀ (p q r : List X)
      → α⇐ ∘ (id ⊗₁ split q) ∘ split p ≈Term ((split p ⊗₁ id) ∘ split (p ++ q)) ∘ assocW p q r
    split-assoc p q r = inv-resp fi-f g-gi (merge-assoc p q r)
      where
        mL : HomTerm ((wires p ⊗₀ wires q) ⊗₀ wires r) (wires (p ++ (q ++ r)))
        mL = merge p ∘ (id ⊗₁ merge q) ∘ α⇒
        fi : HomTerm (wires (p ++ (q ++ r))) ((wires p ⊗₀ wires q) ⊗₀ wires r)
        fi = α⇐ ∘ (id ⊗₁ split q) ∘ split p
        mR : HomTerm ((wires p ⊗₀ wires q) ⊗₀ wires r) (wires ((p ++ q) ++ r))
        mR = merge (p ++ q) ∘ (merge p ⊗₁ id)
        giU : HomTerm (wires ((p ++ q) ++ r)) ((wires p ⊗₀ wires q) ⊗₀ wires r)
        giU = (split p ⊗₁ id) ∘ split (p ++ q)
 
        fi-f : fi ∘ mL ≈Term id
        fi-f = begin
          (α⇐ ∘ (id ⊗₁ split q) ∘ split p) ∘ (merge p ∘ (id ⊗₁ merge q) ∘ α⇒)
            ≈⟨ center (cancelʳ (split∘merge p)) ⟩
          α⇐ ∘ ((id ⊗₁ split q) ∘ ((id ⊗₁ merge q) ∘ α⇒))
            ≈⟨ refl⟩∘⟨ cancelˡ (id⊗-cancel (split∘merge q)) ⟩
          α⇐ ∘ α⇒
            ≈⟨ α⇐∘α⇒≈id ⟩
          id ∎
 
        g-gi : (assocW⁻ p q r ∘ mR) ∘ (giU ∘ assocW p q r) ≈Term id
        g-gi = cancelInner mR-giU ○ assocW⁻∘assocW p q r
          where
            mR-giU : mR ∘ giU ≈Term id
            mR-giU = cancelInner ((⟺ ⊗-∘-dist) ○ ((merge∘split p) ⟩⊗⟨ idˡ) ○ id⊗id≈id) ○ merge∘split (p ++ q)