----------------------------------------------------------------------------------------------------
-- Finite Hereditary Multisets
----------------------------------------------------------------------------------------------------

{- We work with the quotient inductive type of finite hereditary
   multisets, which has been developed in

     Fredrik Nordvall Forsberg, Chuangjie Xu, and Neil Ghani.
     Threee quivalent ordinal notation systems in cubical agda.
     In Proceedings of the 9th ACM SIGPLAN International Conference
     on Certified Programs and Proofs, CPP 2020, page 172–185.
     Association for Computing Machinery, 2020.
-}

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

module FiniteHereditaryMultiset.Base where

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


{- Finite hereditary multisets as a quotient inductive type -}

infixr  ω^_⊕_

data Fhm : Type₀ where
 𝟎 : Fhm
 ω^_⊕_ : Fhm → Fhm → Fhm
 swap : ∀ a b c → ω^ a ⊕ ω^ b ⊕ c ≡ ω^ b ⊕ ω^ a ⊕ c
 trunc : isSet Fhm

private
 variable
  ℓ : Level
  a b c : Fhm

example : ω^ a ⊕ ω^ b ⊕ ω^ c ⊕ 𝟎 ≡ ω^ c ⊕ ω^ b ⊕ ω^ a ⊕ 𝟎
example {a} {b} {c} =
  ω^ a ⊕ ω^ b ⊕ ω^ c ⊕ 𝟎 ≡⟨ swap a b _ ⟩
  ω^ b ⊕ ω^ a ⊕ ω^ c ⊕ 𝟎 ≡⟨ cong (ω^ b ⊕_) (swap a c _) ⟩
  ω^ b ⊕ ω^ c ⊕ ω^ a ⊕ 𝟎 ≡⟨ swap b c _ ⟩
  ω^ c ⊕ ω^ b ⊕ ω^ a ⊕ 𝟎 ∎


{- Induction/elimination principles of Fhm -}

ind : (A : Fhm → Type ℓ)
    → (a₀    : A 𝟎)
    → (_✶_   : ∀ {x y} → A x → A y → A (ω^ x ⊕ y))
    → (✶swap : ∀ {x y z} (a : A x) (b : A y) (c : A z)
             → PathP _ (a ✶ (b ✶ c)) (b ✶ (a ✶ c)))
    → (sv    : ∀ {x} → isSet (A x))
    → ∀ x → A x
ind A a₀ _✶_ ✶swap sv 𝟎 = a₀
ind A a₀ _✶_ ✶swap sv (ω^ x ⊕ y) =
  ind A a₀ _✶_ ✶swap sv x ✶ ind A a₀ _✶_ ✶swap sv y
ind A a₀ _✶_ ✶swap sv (swap x y z i) =
  ✶swap (ind A a₀ _✶_ ✶swap sv x)
        (ind A a₀ _✶_ ✶swap sv y)
        (ind A a₀ _✶_ ✶swap sv z) i
ind A a₀ _✶_ ✶swap sv (trunc _ _ p q i j) =
  isOfHLevel→isOfHLevelDep 
                           (λ x a b → sv {x} a b)
                           _ _
                           (cong (ind A a₀ _✶_ ✶swap sv) p)
                           (cong (ind A a₀ _✶_ ✶swap sv) q)
                           (trunc _ _ p q) i j

-- The recursion principle and the induction principle for propositions
-- are just instances of the above full induction principle.

rec : {A : Type ℓ}
    → isSet A
    → A
    → (_✶_ : A → A → A)
    → (∀ x y z → x ✶ (y ✶ z) ≡ y ✶ (x ✶ z))
    → Fhm → A
rec hset a₀ _✶_ ✶swap = ind _ a₀ _✶_ ✶swap hset

indProp : {P : Fhm → Type ℓ}
        → (∀ x → isProp (P x))
        → P 𝟎
        → (∀ x y → P x → P y → P (ω^ x ⊕ y))
        → ∀ x → P x
indProp pv p₀ _✶_ =
  ind _ p₀ (_✶_ _ _) (λ a b c → toPathP (pv _ _ _)) (isProp→isSet (pv _))


{- Singleton multisets, representing the ω-based exponentiation -}

ω^⟨_⟩ : Fhm → Fhm
ω^⟨ a ⟩ = ω^ a ⊕ 𝟎

𝟏 ω : Fhm
𝟏 = ω^⟨ 𝟎 ⟩
ω = ω^⟨ 𝟏 ⟩