{-# OPTIONS --cubical --safe #-}

module FiniteHereditaryMultiset.HessenbergMultiplication where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Everything

open import FiniteHereditaryMultiset.Base
open import FiniteHereditaryMultiset.HessenbergAddition

infixr  _⊗_

{- Hessenberg multiplication -}

_∔_ : Fhm → Fhm → Fhm
𝟎 ∔ b = 𝟎
(ω^ a ⊕ c) ∔ b = ω^ (a ⊕ b) ⊕ (c ∔ b)
(swap x y z i) ∔ b = swap (x ⊕ b) (y ⊕ b) (z ∔ b) i
(trunc _ _ p q i j) ∔ b = trunc _ _ (cong (_∔ b) p) (cong (_∔ b) q) i j

∔unitr : ∀ a → a ∔ 𝟎 ≡ a
∔unitr = indProp (λ _ → trunc _ _) refl step
 where
  step : ∀ x y → (x ∔ 𝟎) ≡ x → (y ∔ 𝟎) ≡ y → (ω^ x ⊕ y) ∔ 𝟎 ≡ ω^ x ⊕ y
  step x y _ py =
    ω^ (x ⊕ 𝟎) ⊕ (y ∔ 𝟎) ≡⟨ cong (ω^_⊕ (y ∔ 𝟎)) (⊕unitr x) ⟩
    ω^ x ⊕ (y ∔ 𝟎) ≡⟨ cong (ω^ x ⊕_) py ⟩
    ω^ x ⊕ y ∎

∔-r-distributive-over-⊕ : ∀ a b c → (a ⊕ b) ∔ c ≡ (a ∔ c) ⊕ (b ∔ c)
∔-r-distributive-over-⊕ = indProp hprop base step
 where
  P : Fhm → Type₀
  P a = ∀ b c → (a ⊕ b) ∔ c ≡ (a ∔ c) ⊕ (b ∔ c)
  hprop : ∀ a → isProp (P a)
  hprop a p q i b c = trunc _ _ (p b c) (q b c) i
  base : P 𝟎
  base _ _ = refl
  step : ∀ x y → P x → P y → P (ω^ x ⊕ y)
  step x y px py b c = cong (ω^ (x ⊕ c) ⊕_) (py b c)

∔[⊕]≡[∔]∔ : ∀ a b c → a ∔ (b ⊕ c) ≡ (a ∔ b) ∔ c
∔[⊕]≡[∔]∔ = indProp hprop base step
 where
  P : Fhm → Type₀
  P a = ∀ b c → a ∔ (b ⊕ c) ≡ (a ∔ b) ∔ c
  hprop : ∀ a → isProp (P a)
  hprop a p q i b c = trunc _ _ (p b c) (q b c) i
  base : P 𝟎
  base b c = refl
  step : ∀ x y → P x → P y → P (ω^ x ⊕ y)
  step x y px py b c =
    ω^ (x ⊕ (b ⊕ c)) ⊕ (y ∔ (b ⊕ c)) ≡⟨ cong (ω^ (x ⊕ (b ⊕ c)) ⊕_) (py b c) ⟩
    ω^ (x ⊕ (b ⊕ c)) ⊕ ((y ∔ b) ∔ c) ≡⟨ cong (ω^_⊕ ((y ∔ b) ∔ c)) (⊕assoc x b c) ⟩
    ω^ ((x ⊕ b) ⊕ c) ⊕ ((y ∔ b) ∔ c) ∎

_⊗_ : Fhm → Fhm → Fhm
a ⊗ 𝟎 = 𝟎
a ⊗ (ω^ b ⊕ c) = (a ∔ b) ⊕ (a ⊗ c)
a ⊗ (swap x y z i) = ⊕swap (a ∔ x) (a ∔ y) (a ⊗ z) i
a ⊗ (trunc _ _ p q i j) = trunc _ _ (cong (a ⊗_) p) (cong (a ⊗_) q) i j

zero⊗ : ∀ a → 𝟎 ⊗ a ≡ 𝟎
zero⊗ = indProp (λ _ → trunc _ _) refl (λ _ _ _ p → p)

⊗-l-distributive-over-⊕ : ∀ a b c → a ⊗ (b ⊕ c) ≡ a ⊗ b ⊕ a ⊗ c
⊗-l-distributive-over-⊕ a b c = indProp hprop base step b a c
 where
  P : Fhm → Type₀
  P b = ∀ a c → a ⊗ (b ⊕ c) ≡ a ⊗ b ⊕ a ⊗ c
  hprop : ∀ b → isProp (P b)
  hprop b p q i a c = trunc _ _ (p a c) (q a c) i
  base : P 𝟎
  base _ _ = refl
  step : ∀ x y → P x → P y → P (ω^ x ⊕ y)
  step x y px py a c =
    (a ∔ x) ⊕ a ⊗ (y ⊕ c) ≡⟨ cong ((a ∔ x) ⊕_) (py a c) ⟩
    (a ∔ x) ⊕ (a ⊗ y ⊕ a ⊗ c) ≡⟨ ⊕assoc (a ∔ x) (a ⊗ y) (a ⊗ c) ⟩
    ((a ∔ x) ⊕ a ⊗ y) ⊕ a ⊗ c ∎

⊗-r-distributive-over-⊕ : ∀ a b c → (a ⊕ b) ⊗ c ≡ a ⊗ c ⊕ b ⊗ c
⊗-r-distributive-over-⊕ a b c = indProp hprop base step c a b
 where
  P : Fhm → Type₀
  P c = ∀ a b → (a ⊕ b) ⊗ c ≡ a ⊗ c ⊕ b ⊗ c
  hprop : ∀ b → isProp (P b)
  hprop b p q i a c = trunc _ _ (p a c) (q a c) i
  base : P 𝟎
  base _ _ = refl
  step : ∀ x y → P x → P y → P (ω^ x ⊕ y)
  step x y px py a b =
     ((a ⊕ b) ∔ x) ⊕ (a ⊕ b) ⊗ y
    ≡⟨ cong (((a ⊕ b) ∔ x) ⊕_) (py a b) ⟩
     ((a ⊕ b) ∔ x) ⊕ (a ⊗ y) ⊕ (b ⊗ y)
    ≡⟨ ⊕assoc ((a ⊕ b) ∔ x) (a ⊗ y) (b ⊗ y) ⟩
     (((a ⊕ b) ∔ x) ⊕ (a ⊗ y)) ⊕ (b ⊗ y)
    ≡⟨ cong (λ z → (z ⊕ (a ⊗ y)) ⊕ (b ⊗ y)) (∔-r-distributive-over-⊕ a b x) ⟩
     (((a ∔ x) ⊕ (b ∔ x)) ⊕ (a ⊗ y)) ⊕ (b ⊗ y)
    ≡⟨ cong (_⊕ (b ⊗ y)) ((⊕assoc (a ∔ x) (b ∔ x) (a ⊗ y)) ⁻¹) ⟩
     ((a ∔ x) ⊕ (b ∔ x) ⊕ (a ⊗ y)) ⊕ (b ⊗ y)
    ≡⟨ cong (λ z → ((a ∔ x) ⊕ z) ⊕ (b ⊗ y)) (⊕comm (b ∔ x) (a ⊗ y)) ⟩
     ((a ∔ x) ⊕ (a ⊗ y) ⊕ (b ∔ x)) ⊕ (b ⊗ y)
    ≡⟨ cong (_⊕ (b ⊗ y)) (⊕assoc (a ∔ x) (a ⊗ y) (b ∔ x)) ⟩
     (((a ∔ x) ⊕ a ⊗ y) ⊕ (b ∔ x)) ⊕ b ⊗ y
    ≡⟨ ⊕assoc ((a ∔ x) ⊕ a ⊗ y) (b ∔ x) (b ⊗ y) ⁻¹ ⟩
     ((a ∔ x) ⊕ a ⊗ y) ⊕ (b ∔ x) ⊕ b ⊗ y  ∎

⊗-∔-assoc : ∀ a b c → a ⊗ (b ∔ c) ≡ (a ⊗ b) ∔ c
⊗-∔-assoc a b c = indProp hprop base step b a c
 where
  P : Fhm → Type₀
  P b = ∀ a c → a ⊗ (b ∔ c) ≡ (a ⊗ b) ∔ c
  hprop : ∀ b → isProp (P b)
  hprop b p q i a c = trunc _ _ (p a c) (q a c) i
  base : P 𝟎
  base _ _ = refl
  step : ∀ x y → P x → P y → P (ω^ x ⊕ y)
  step x y px py a c =
    (a ∔ (x ⊕ c)) ⊕ a ⊗ (y ∔ c) ≡⟨ cong ((a ∔ (x ⊕ c)) ⊕_) (py a c) ⟩
    (a ∔ (x ⊕ c)) ⊕ (a ⊗ y ∔ c) ≡⟨ cong (_⊕ (a ⊗ y ∔ c)) (∔[⊕]≡[∔]∔ a x c) ⟩
    ((a ∔ x) ∔ c) ⊕ (a ⊗ y ∔ c) ≡⟨ (∔-r-distributive-over-⊕ (a ∔ x) (a ⊗ y) c) ⁻¹ ⟩
    ((a ∔ x) ⊕ a ⊗ y) ∔ c ∎

{- _⊗_ is associative. -}

⊗assoc : ∀ a b c → a ⊗ (b ⊗ c) ≡ (a ⊗ b) ⊗ c
⊗assoc a b c = indProp hprop base step c a b
 where
  P : Fhm → Type₀
  P c = ∀ a b → a ⊗ (b ⊗ c) ≡ (a ⊗ b) ⊗ c
  hprop : ∀ c → isProp (P c)
  hprop c p q i a b = trunc _ _ (p a b) (q a b) i
  base : P 𝟎
  base _ _ = refl
  step : ∀ x y → P x → P y → P (ω^ x ⊕ y)
  step x y px py a b =
    a ⊗ ((b ∔ x) ⊕ b ⊗ y) ≡⟨ ⊗-l-distributive-over-⊕ a (b ∔ x) (b ⊗ y) ⟩
    a ⊗ (b ∔ x) ⊕ a ⊗ (b ⊗ y) ≡⟨ cong (_⊕ a ⊗ (b ⊗ y)) (⊗-∔-assoc a b x) ⟩
    ((a ⊗ b) ∔ x) ⊕ a ⊗ (b ⊗ y) ≡⟨ cong (((a ⊗ b) ∔ x) ⊕_) (py a b) ⟩
    ((a ⊗ b) ∔ x) ⊕ (a ⊗ b) ⊗ y ∎

ω^⟨a⟩⊗b≡b∔a : ∀ a b → ω^⟨ a ⟩ ⊗ b ≡ b ∔ a
ω^⟨a⟩⊗b≡b∔a a b = indProp hprop base step b a
 where
  P : Fhm → Type₀
  P b = ∀ a → ω^⟨ a ⟩ ⊗ b ≡ b ∔ a
  hprop : ∀ a → isProp (P a)
  hprop b p q i a = trunc _ _ (p a) (q a) i
  base : P 𝟎
  base a = refl
  step : ∀ x y → P x → P y → P (ω^ x ⊕ y)
  step x y px py a =
    (ω^ (a ⊕ x) ⊕ (ω^⟨ a ⟩ ⊗ y)) ≡⟨ cong (ω^_⊕ (ω^⟨ a ⟩ ⊗ y)) (⊕comm a x) ⟩
    (ω^ (x ⊕ a) ⊕ (ω^⟨ a ⟩ ⊗ y)) ≡⟨ cong (ω^ (x ⊕ a) ⊕_) (py a) ⟩
    (ω^ (x ⊕ a) ⊕ (y ∔ a)) ∎

{- _⊗_ is commutative. -}

⊗comm : ∀ a b → a ⊗ b ≡ b ⊗ a
⊗comm = indProp hprop base step
 where
  P : Fhm → Type₀
  P a = ∀ b → a ⊗ b ≡ b ⊗ a
  hprop : ∀ a → isProp (P a)
  hprop a p q i b = trunc _ _ (p b) (q b) i
  base : P 𝟎
  base = zero⊗
  step : ∀ x y → P x → P y → P (ω^ x ⊕ y)
  step x y px py b =
    (ω^ x ⊕ y) ⊗ b ≡⟨ cong (_⊗ b) (ω^⊕≡ω^⟨⟩⊕ x y) ⟩
    (ω^⟨ x ⟩ ⊕ y) ⊗ b ≡⟨ ⊗-r-distributive-over-⊕ ω^⟨ x ⟩ y b ⟩
    ω^⟨ x ⟩ ⊗ b ⊕ y ⊗ b ≡⟨ cong (_⊕ y ⊗ b) (ω^⟨a⟩⊗b≡b∔a x b) ⟩
    (b ∔ x) ⊕ y ⊗ b ≡⟨ cong ((b ∔ x) ⊕_) (py b) ⟩
    (b ∔ x) ⊕ b ⊗ y ∎