----------------------------------------------------------------------------------------------------
-- Hessenberg arithmetic operations on Cantor Normal Forms
----------------------------------------------------------------------------------------------------

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

module CantorNormalForm.HessenbergArithmetic where

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

open import CantorNormalForm.Everything
import FiniteHereditaryMultiset.Everything as F
open import Interpretations.CnfEqFhm


{- Hessenberg addition of Cantor Normal Forms -}

_⊕_ : Cnf → Cnf → Cnf
_⊕_ = transport (λ i → (Cnf≡Fhm ⁻¹) i → (Cnf≡Fhm ⁻¹) i → (Cnf≡Fhm ⁻¹) i) F._⊕_

⊕Path : PathP (λ i → (Cnf≡Fhm ⁻¹) i → (Cnf≡Fhm ⁻¹) i → (Cnf≡Fhm ⁻¹) i) F._⊕_ _⊕_
⊕Path i = transp (λ j → (Cnf≡Fhm ⁻¹) (i ∧ j) → (Cnf≡Fhm ⁻¹) (i ∧ j) → (Cnf≡Fhm ⁻¹) (i ∧ j)) (~ i) F._⊕_

⊕assoc : ∀ a b c → a ⊕ (b ⊕ c) ≡ (a ⊕ b) ⊕ c
⊕assoc = transport (λ i → ∀ (a b c : (Cnf≡Fhm ⁻¹) i) → ⊕Path i a (⊕Path i b c) ≡ ⊕Path i (⊕Path i a b) c) F.⊕assoc

⊕comm : ∀ a b → a ⊕ b ≡ b ⊕ a
⊕comm = transport (λ i → ∀ (a b : (Cnf≡Fhm ⁻¹) i) → ⊕Path i a b ≡ ⊕Path i b a) F.⊕comm


{- Hessenberg multiplication of Cantor Normal Forms -}

_⊗_ : Cnf → Cnf → Cnf
_⊗_ = transport (λ i → (Cnf≡Fhm ⁻¹) i → (Cnf≡Fhm ⁻¹) i → (Cnf≡Fhm ⁻¹) i) F._⊗_

⊗Path : PathP (λ i → (Cnf≡Fhm ⁻¹) i → (Cnf≡Fhm ⁻¹) i → (Cnf≡Fhm ⁻¹) i) F._⊗_ _⊗_
⊗Path i = transp (λ j → (Cnf≡Fhm ⁻¹) (i ∧ j) → (Cnf≡Fhm ⁻¹) (i ∧ j) → (Cnf≡Fhm ⁻¹) (i ∧ j)) (~ i) F._⊗_

⊗assoc : ∀ a b c → a ⊗ (b ⊗ c) ≡ (a ⊗ b) ⊗ c
⊗assoc = transport (λ i → ∀ (a b c : (Cnf≡Fhm ⁻¹) i) → ⊗Path i a (⊗Path i b c) ≡ ⊗Path i (⊗Path i a b) c) F.⊗assoc

⊗comm : ∀ a b → a ⊗ b ≡ b ⊗ a
⊗comm = transport (λ i → ∀ (a b : (Cnf≡Fhm ⁻¹) i) → ⊗Path i a b ≡ ⊗Path i b a) F.⊗comm