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

module FiniteHereditaryMultiset.HessenbergAddition where

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

open import FiniteHereditaryMultiset.Base

infixr  _⊕_

{- Hessenberg addition, implemented as multiset concatenation -}

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

⊕unitr : (a : Fhm) → a ⊕ 𝟎 ≡ a
⊕unitr = indProp (λ _ → trunc _ _) base step
 where
  base : 𝟎 ⊕ 𝟎 ≡ 𝟎
  base = refl
  step : ∀ x y → _ → y ⊕ 𝟎 ≡ y
       → (ω^ x ⊕ y) ⊕ 𝟎 ≡ ω^ x ⊕ y
  step x _ _ = cong (ω^ x ⊕_)

{- _⊕_ is associative. -}

⊕assoc : ∀ a b c → a ⊕ (b ⊕ c) ≡ (a ⊕ b) ⊕ c
⊕assoc = indProp hprop base step
 where
  P : Fhm → Type₀
  P a = ∀ b c → a ⊕ b ⊕ c ≡ (a ⊕ b) ⊕ c
  hprop : ∀ a → isProp (P a)
  hprop _ 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 _ p b c = cong (ω^ x ⊕_) (p b c)

ω^⊕≡⊕ω^⟨⟩ : (a b : Fhm) → (ω^ a ⊕ b) ≡ b ⊕ ω^⟨ a ⟩
ω^⊕≡⊕ω^⟨⟩ a = indProp (λ _ → trunc _ _) base step
 where
  P : Fhm → Type₀
  P b = (ω^ a ⊕ b) ≡ b ⊕ ω^⟨ a ⟩
  base : P 𝟎
  base = refl
  step : ∀ x y → P x → P y → P (ω^ x ⊕ y)
  step x y _ p = swap a x y ∙ cong (ω^ x ⊕_) p

{- _⊕_ is commutative -}

⊕comm : ∀ a b → a ⊕ b ≡ b ⊕ a
⊕comm a = indProp (λ _ → trunc _ _) base step
 where
  P : Fhm → Type₀
  P b = a ⊕ b ≡ b ⊕ a
  base : P 𝟎
  base = ⊕unitr a
  step : ∀ x y → P x → P y → P (ω^ x ⊕ y)
  step x y _ p =
      a ⊕ (ω^ x ⊕ y)
    ≡⟨ cong (a ⊕_) (ω^⊕≡⊕ω^⟨⟩ x y) ⟩
      a ⊕ (y ⊕ ω^⟨ x ⟩)
    ≡⟨ ⊕assoc a y ω^⟨ x ⟩ ⟩
      (a ⊕ y) ⊕ ω^⟨ x ⟩
    ≡⟨ cong (_⊕ ω^⟨ x ⟩) p ⟩
      (y ⊕ a) ⊕ ω^⟨ x ⟩
    ≡⟨ (ω^⊕≡⊕ω^⟨⟩ x (y ⊕ a)) ⁻¹ ⟩
      (ω^ x ⊕ y) ⊕ a  ∎

ω^⊕≡ω^⟨⟩⊕ : ∀ a b → (ω^ a ⊕ b) ≡ ω^⟨ a ⟩ ⊕ b
ω^⊕≡ω^⟨⟩⊕ a b =
  (ω^ a ⊕ b) ≡⟨ ω^⊕≡⊕ω^⟨⟩ a b ⟩
  b ⊕ ω^⟨ a ⟩ ≡⟨ ⊕comm b ω^⟨ a ⟩ ⟩
  ω^⟨ a ⟩ ⊕ b ∎

⊕swap : ∀ a b c → a ⊕ b ⊕ c ≡ b ⊕ a ⊕ c
⊕swap a b c =
  a ⊕ (b ⊕ c) ≡⟨ ⊕assoc a b c ⟩
  (a ⊕ b) ⊕ c ≡⟨ cong (_⊕ c) (⊕comm a b) ⟩
  (b ⊕ a) ⊕ c ≡⟨ (⊕assoc b a c)⁻¹ ⟩
  b ⊕ (a ⊕ c) ∎