Martin Escardo and Tom de Jong, 9th December 2023.

We discuss "hereditarily finitely linearly ordered iterative
multisets". Notice that this is data, rather then property.

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan hiding (_^_)
open import UF.Univalence

module Iterative.Multisets-HFLO
        (ua : Univalence)
        (𝓀 : Universe)
       where

open import Iterative.Multisets 𝓀
open import Iterative.Multisets-Addendum ua 𝓀
open import UF.Base
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Subsingletons
open import UF.UA-FunExt
open import W.Type

private
 𝓀⁺ : Universe
 𝓀⁺ = 𝓀 ⁺

 fe : Fun-Ext
 fe = Univalence-gives-Fun-Ext ua

 fe' : FunExt
 fe' 𝓀 π“₯ = fe {𝓀} {π“₯}

open import Fin.Bishop
open import Fin.Type

hflo-data : 𝕄 β†’ 𝓀 Μ‡
hflo-data (ssup X Ο†) = finite-linear-order X
                     Γ— ((x : X) β†’ hflo-data (Ο† x))

hflo-data-gives-finite-linear-order
 : (M : 𝕄)
 β†’ hflo-data M
 β†’ finite-linear-order (𝕄-root M)
hflo-data-gives-finite-linear-order (ssup x Ο†) = pr₁

𝕄-subtrees-have-hflo-data
 : (M : 𝕄)
 β†’ hflo-data M
 β†’ (x : 𝕄-root M) β†’ hflo-data (𝕄-forest M x)
𝕄-subtrees-have-hflo-data (ssup x Ο†) = prβ‚‚

ℍ : 𝓀⁺ Μ‡
ℍ = Ξ£ M κž‰ 𝕄 , hflo-data M

ℍ-underlying-mset : ℍ β†’ 𝕄
ℍ-underlying-mset = pr₁

hflo-structure : (H : ℍ) β†’ hflo-data (ℍ-underlying-mset H)
hflo-structure = prβ‚‚

\end{code}

Examples. We will use the superscript H to indicate elements of the
type ℍ.

\begin{code}

𝟘ᴹ-hflo-data : hflo-data 𝟘ᴹ
𝟘ᴹ-hflo-data = (0 , f) , (Ξ» (x : 𝟘) β†’ 𝟘-elim x)
 where
  f : 𝟘 {𝓀} ≃ 𝟘 {𝓀₀}
  f = one-𝟘-only

𝟘ᴴ : ℍ
𝟘ᴴ = 𝟘ᴹ , 𝟘ᴹ-hflo-data

open import UF.Equiv-FunExt

𝟘ᴴ-equality : (H : ℍ)
            β†’ is-empty (𝕄-root (ℍ-underlying-mset H))
            β†’ 𝟘ᴴ ＝ H
𝟘ᴴ-equality (ssup X Ο† , (0 , f) , Ξ΄) e =
 to-Σ-＝
  ((to-𝕄-＝
     (eqtoid (ua 𝓀) 𝟘 X (≃-sym (f ● one-𝟘-only)) ,
      dfunext fe (Ξ» (x : 𝟘) β†’ 𝟘-elim x))) ,
    I)
 where
  I : {d : hflo-data (ssup X Ο†)} β†’ d ＝ (zero , f) , Ξ΄
  I {(zero , f') , Ξ΄'} =
    to-Σ-＝
     (to-Σ-＝
       (refl ,
        to-subtype-＝
         (being-equiv-is-prop fe')
         (dfunext fe (Ξ» x β†’ 𝟘-elim (⌜ f ⌝ x)))) ,
      dfunext fe (Ξ» x β†’ 𝟘-elim (⌜ f ⌝ x)))
  I {(succ n' , f') , δ'} = 𝟘-elim (e (⌜ f' ⌝⁻¹ 𝟎))
𝟘ᴴ-equality (ssup X Ο† , (succ n , f) , Ξ΄) e = 𝟘-elim (e (⌜ f ⌝⁻¹ 𝟎))

πŸ™α΄Ή-hflo-data : hflo-data πŸ™α΄Ή
πŸ™α΄Ή-hflo-data = (1 , f) , (Ξ» ⋆ β†’ 𝟘ᴹ-hflo-data)
 where
  f : πŸ™ {𝓀} ≃ 𝟘 {𝓀₀} + πŸ™ {𝓀₀}
  f = 𝟘-lneutral''

πŸ™α΄΄ : ℍ
πŸ™α΄΄ = πŸ™α΄Ή , πŸ™α΄Ή-hflo-data

𝟚ᴹ-hflo-data : hflo-data 𝟚ᴹ
𝟚ᴹ-hflo-data = πŸ™+πŸ™-natural-finite-linear-order ,
               dep-cases (Ξ» _ β†’ 𝟘ᴹ-hflo-data) (Ξ» _ β†’ πŸ™α΄Ή-hflo-data)

𝟚ᴴ : ℍ
𝟚ᴴ = 𝟚ᴹ , 𝟚ᴹ-hflo-data

open import Fin.ArithmeticViaEquivalence

Ξ£α΄Ή-hflo-data : {X : 𝓀 Μ‡ }
               (A : X β†’ 𝕄)
             β†’ finite-linear-order X
             β†’ ((x : X) β†’ hflo-data (A x))
             β†’ hflo-data (Ξ£α΄Ή A)
Ξ£α΄Ή-hflo-data {X} A (n , f) A-hflo = (βˆ‘ a , h) , Ξ΄
 where
  u : (x : X) β†’ Ξ£ m κž‰ β„• , 𝕄-root (A x) ≃ Fin m
  u x = hflo-data-gives-finite-linear-order (A x) (A-hflo x)

  a : Fin n β†’ β„•
  a i = pr₁ (u (⌜ f ⌝⁻¹ i))

  b : (i : Fin n) β†’ 𝕄-root (A (⌜ f ⌝⁻¹ i)) ≃ Fin (a i)
  b i = prβ‚‚ (u (⌜ f ⌝⁻¹ i))

  h = (Ξ£ x κž‰ X , 𝕄-root (A x))               β‰ƒβŸ¨ hβ‚€ ⟩
      (Ξ£ i κž‰ Fin n , 𝕄-root (A (⌜ f ⌝⁻¹ i))) β‰ƒβŸ¨ h₁ ⟩
      (Ξ£ i κž‰ Fin n , Fin (a i))              β‰ƒβŸ¨ hβ‚‚ ⟩
      Fin (βˆ‘ a)                              β– 
       where
        hβ‚€ = ≃-sym (Ξ£-change-of-variable-≃ (Ξ» x β†’ 𝕄-root (A x)) (≃-sym f))
        h₁ = Ξ£-cong b
        hβ‚‚ = ≃-sym (βˆ‘-property a)

  Ξ΄ : ((x , y) : Ξ£ x κž‰ X , 𝕄-root (A x)) β†’ hflo-data (𝕄-forest (A x) y)
  Ξ΄ (x , y) = 𝕄-subtrees-have-hflo-data (A x) (A-hflo x) y

Ξ α΄Ή-hflo-data : {X : 𝓀 Μ‡ }
               (A : X β†’ 𝕄)
             β†’ finite-linear-order X
             β†’ ((x : X) β†’ hflo-data (A x))
             β†’ hflo-data (Ξ α΄Ή A)
Πᴹ-hflo-data {X} A (n , f) A-hflo = (∏ fe a , h) , δ
 where
  u : (x : X) β†’ Ξ£ m κž‰ β„• , 𝕄-root (A x) ≃ Fin m
  u x = hflo-data-gives-finite-linear-order (A x) (A-hflo x)

  a : Fin n β†’ β„•
  a i = pr₁ (u (⌜ f ⌝⁻¹ i))

  b : (i : Fin n) β†’ 𝕄-root (A (⌜ f ⌝⁻¹ i)) ≃ Fin (a i)
  b i = prβ‚‚ (u (⌜ f ⌝⁻¹ i))

  h = (Ξ  x κž‰ X , 𝕄-root (A x))               β‰ƒβŸ¨ hβ‚€ ⟩
      (Ξ  i κž‰ Fin n , 𝕄-root (A (⌜ f ⌝⁻¹ i))) β‰ƒβŸ¨ h₁ ⟩
      (Ξ  i κž‰ Fin n , Fin (a i))              β‰ƒβŸ¨ hβ‚‚ ⟩
      Fin (∏ fe a)                              β– 
       where
        hβ‚€ = ≃-sym (Ξ -change-of-variable-≃ fe' (Ξ» x β†’ 𝕄-root (A x)) (≃-sym f))
        h₁ = Ξ -cong fe fe b
        hβ‚‚ = ≃-sym (∏-property fe a)

  v : (x : X) (y : 𝕄-root (A x)) β†’ hflo-data (𝕄-forest (A x) y)
  v x = 𝕄-subtrees-have-hflo-data (A x) (A-hflo x)

  Ξ΄ : (g : Ξ  x κž‰ X , 𝕄-root (A x)) β†’ hflo-data (Ξ£α΄Ή (Ξ» x β†’ 𝕄-forest (A x) (g x)))
  Ξ΄ g = Ξ£α΄Ή-hflo-data (Ξ» x β†’ 𝕄-forest (A x) (g x)) (n , f) (Ξ» x β†’ v x (g x))

+α΄Ή-hflo-data : (M N : 𝕄)
             β†’ hflo-data M
             β†’ hflo-data N
             β†’ hflo-data (M +α΄Ή N)
+α΄Ή-hflo-data M N h k =
 Ξ£α΄Ή-hflo-data (cases (Ξ» _ β†’ M) (Ξ» _ β†’ N))
  πŸ™+πŸ™-natural-finite-linear-order
  (dep-cases (Ξ» _ β†’ h) (Ξ» _ β†’ k))

Γ—α΄Ή-hflo-data : (M N : 𝕄)
             β†’ hflo-data M
             β†’ hflo-data N
             β†’ hflo-data (M Γ—α΄Ή N)
Γ—α΄Ή-hflo-data M N h k =
 Ξ α΄Ή-hflo-data (cases (Ξ» _ β†’ M) (Ξ» _ β†’ N))
  πŸ™+πŸ™-natural-finite-linear-order
  (dep-cases (Ξ» _ β†’ h) (Ξ» _ β†’ k))

Γ—α΄Ή'-hflo-data : (M N : 𝕄)
             β†’ hflo-data M
             β†’ hflo-data N
             β†’ hflo-data (M Γ—α΄Ή' N)
Γ—α΄Ή'-hflo-data (ssup X Ο†) (ssup Y Ξ³) ((n , f) , u) ((m , g) , v) = (n Γ—' m ,
  (X Γ— Y        β‰ƒβŸ¨ Γ—-cong f g ⟩
  Fin n Γ— Fin m β‰ƒβŸ¨ ≃-sym (FinΓ—homo n m) ⟩
  Fin (n Γ—' m)  β– )) ,
  (Ξ» (x , y) β†’ Γ—α΄Ή'-hflo-data (Ο† x) (Ξ³ y) (u x) (v y))

_+α΄΄_ _Γ—α΄΄_ _Γ—α΄΄'_ : ℍ β†’ ℍ β†’ ℍ
(M , h) +α΄΄ (N , k) = M +α΄Ή N , +α΄Ή-hflo-data M N h k
(M , h) Γ—α΄΄ (N , k) = M Γ—α΄Ή N , Γ—α΄Ή-hflo-data M N h k
(M , h) Γ—α΄΄' (N , k) = M Γ—α΄Ή' N , Γ—α΄Ή'-hflo-data M N h k

\end{code}

TODO. Define Ξ£α΄΄ and Ξ α΄΄. (Boilerplate.)

We now develop a representation of elements of ℍ for the sake of being
able to exhibit examples explicitly and visually.

\begin{code}

data _^_ (X : π“₯ Μ‡ ) : β„• β†’ π“₯ Μ‡ where
 Β·   : X ^ 0
 _,_ : {n : β„•} β†’ X β†’ X ^ n β†’ X ^ (succ n)

data π•Š : 𝓀 Μ‡ where
 [_] : {n : β„•} β†’ π•Š ^ n β†’ π•Š

to-vector : (n : β„•) β†’ (Fin n β†’ π•Š) β†’ π•Š ^ n
to-vector 0        f = Β·
to-vector (succ n) f = f 𝟎 , to-vector n (f ∘ suc)

to-π•Š-curried : (M : 𝕄) β†’ hflo-data M β†’ π•Š
to-π•Š-curried (ssup X Ο†) ((n , f) , Ξ΄) =
 [ to-vector n (Ξ» (i : Fin n) β†’ to-π•Š-curried (Ο† (⌜ f ⌝⁻¹ i)) (Ξ΄ (⌜ f ⌝⁻¹ i))) ]

to-π•Š : ℍ β†’ π•Š
to-π•Š = uncurry to-π•Š-curried

\end{code}

Examples.

\begin{code}

private
 s = to-π•Š

πŸ›α΄΄ πŸ›α΄΄' : ℍ
πŸ›α΄΄  = πŸ™α΄΄ +α΄΄ 𝟚ᴴ
πŸ›α΄΄' = 𝟚ᴴ +α΄΄ πŸ™α΄΄

𝟘˒ πŸ™Λ’ 𝟚˒ πŸ›Λ’ πŸ›Λ’' : π•Š
𝟘˒  = s 𝟘ᴴ
πŸ™Λ’  = s πŸ™α΄΄
𝟚˒  = s 𝟚ᴴ
πŸ›Λ’  = s πŸ›α΄΄
πŸ›Λ’' = s πŸ›α΄΄'

examplesΛ’
 : ( 𝟘˒  ＝ [ · ]                                           )
 Γ— ( πŸ™Λ’  ＝ [ 𝟘˒ , Β· ]                                      )
 Γ— ( 𝟚˒  ＝ [ 𝟘˒ , πŸ™Λ’ , Β· ]                                 )
 Γ— ( πŸ›Λ’  ＝ [ 𝟘˒ , πŸ™Λ’ , 𝟘˒ , Β· ]                            )
 Γ— ( πŸ›Λ’' ＝ [ 𝟘˒ , 𝟘˒ , πŸ™Λ’ , Β· ]                            )
 Γ— ( s (𝟚ᴴ Γ—α΄΄ 𝟚ᴴ) ＝ [ 𝟘˒ , πŸ™Λ’ , πŸ™Λ’ , [ 𝟘˒ , 𝟘˒ , Β· ] , Β· ] )
 Γ— ( s (𝟚ᴴ Γ—α΄΄' 𝟚ᴴ) ＝ [ 𝟘˒ , 𝟘˒ , 𝟘˒ , πŸ™Λ’ , Β· ]             )
 Γ— ( s (𝟘ᴴ +α΄΄ πŸ™α΄΄) ＝ πŸ™Λ’                                     )
 Γ— ( s (πŸ™α΄΄ +α΄΄ 𝟘ᴴ) ＝ πŸ™Λ’                                     )
 Γ— ( s (πŸ™α΄΄ +α΄΄ πŸ™α΄΄) ＝ [ 𝟘˒ , 𝟘˒ , Β· ]                        )
 Γ— ( s (πŸ›α΄΄ +α΄΄ πŸ›α΄΄) ＝ [ 𝟘˒ , πŸ™Λ’ , 𝟘˒ , 𝟘˒ , πŸ™Λ’ , 𝟘˒ , Β· ]    )
 Γ— ( s (πŸ›α΄΄ Γ—α΄΄ πŸ›α΄΄) ＝ [ 𝟘˒ , πŸ™Λ’ , 𝟘˒ , πŸ™Λ’ ,
                      [ 𝟘˒ , 𝟘˒ , · ] ,
                      πŸ™Λ’ , 𝟘˒ , πŸ™Λ’ , 𝟘˒ , Β· ]               )
 Γ— ( s (πŸ›α΄΄ Γ—α΄΄' πŸ›α΄΄) ＝ [ 𝟘˒ , 𝟘˒ , 𝟘˒ , 𝟘˒ ,
                        πŸ™Λ’ , 𝟘˒ , 𝟘˒ , 𝟘˒ , 𝟘˒ , Β· ]        )
 Γ— ( s (πŸ›α΄΄' Γ—α΄΄ πŸ›α΄΄') ＝ [ 𝟘˒ , 𝟘˒ , πŸ™Λ’ , 𝟘˒ ,
                         𝟘˒ , πŸ™Λ’ , πŸ™Λ’ , πŸ™Λ’ ,
                         [ 𝟘˒ , 𝟘˒ , · ] , · ]              )
examplesΛ’ = refl , refl , refl , refl , refl , refl , refl ,
            refl , refl , refl , refl , refl , refl , refl

\end{code}