Martin Escardo & Tom de Jong, June 2023.

Iterative multisets.

See the module Iterative.index for bibliographic references regarding
this file. All the results of this file are in HΓ₯kon Gylterud [3].

\begin{code}

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

open import MLTT.Spartan

module Iterative.Multisets
        (𝓀 : Universe)
       where

open import UF.Base
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Size
open import UF.Subsingletons
open import UF.UA-FunExt
open import UF.Univalence

open import W.Type
open import W.Properties (𝓀 Μ‡) id

private
 𝓀⁺ : Universe
 𝓀⁺ = 𝓀 ⁺

\end{code}

The type of iterative multisets:

\begin{code}

𝕄 : 𝓀⁺ Μ‡
𝕄 = W (𝓀 Μ‡ ) id

\end{code}

This is equivalent to the following alternative definition.

\begin{code}

private

 data 𝕄' : 𝓀⁺ Μ‡ where
  ssup : (X : 𝓀 Μ‡ ) (Ο† : X β†’ 𝕄') β†’ 𝕄'

 𝕄-to-𝕄' : 𝕄 β†’ 𝕄'
 𝕄-to-𝕄' (ssup X Ο†) = ssup X (Ξ» x β†’ 𝕄-to-𝕄' (Ο† x))

 𝕄'-to-𝕄 : 𝕄' β†’ 𝕄
 𝕄'-to-𝕄 (ssup X Ο†) = ssup X (Ξ» x β†’ 𝕄'-to-𝕄 (Ο† x))

\end{code}

Maybe add the proof that the above two functions are mutually
inverse. But the only point of adding them is to make sure that the
above comment remains valid if any change is made in the code, and the
above two definitions seem to be enough for that purpose.

Aside. Every W-type can be mapped to 𝕄 as follows:

\begin{code}

W-to-𝕄 : {X : 𝓀 Μ‡ } {A : X β†’ 𝓀 Μ‡ }
       β†’ W X A β†’ 𝕄
W-to-𝕄 {X} {A} (ssup x f) = ssup (A x) (Ξ» a β†’ W-to-𝕄 (f a))

\end{code}

TODO. Is the above remark relevant in any way?

In the case of ordinals, "ssup" stands for "strong supremum", "strict
supremum" or "supremum of successors". See the module Iterative.Ordinals.

The two destructors:

\begin{code}

𝕄-root : 𝕄 β†’ 𝓀 Μ‡
𝕄-root = W-root

𝕄-forest : (M : 𝕄) β†’ 𝕄-root M β†’ 𝕄
𝕄-forest = W-forest

\end{code}

The following properties of the above two destructors hold
definitionally;

\begin{code}

𝕄-ssup-root : (X : 𝓀 Μ‡ ) (Ο† : X β†’ 𝕄)
            β†’ 𝕄-root (ssup X Ο†) ＝ X
𝕄-ssup-root = W-ssup-root

𝕄-ssup-forest : (X : 𝓀 Μ‡ ) (Ο† : X β†’ 𝕄)
              β†’ 𝕄-forest (ssup X Ο†) ＝ Ο†
𝕄-ssup-forest = W-ssup-forest

\end{code}

But the Ξ·-law holds only up to an identification:

\begin{code}

𝕄-Ξ· : (M : 𝕄)
    β†’ ssup (𝕄-root M) (𝕄-forest M) ＝ M
𝕄-Ξ· = W-Ξ·

\end{code}

The membership relation for multisets:

\begin{code}

_⁅_ : 𝕄 β†’ 𝕄 β†’ 𝓀⁺ Μ‡
M ⁅ N = Ξ£ x κž‰ 𝕄-root N , 𝕄-forest N x ＝ M

\end{code}

The relation M ⁅ N can hold in multiple ways in general. We can think
of M ⁅ N as measuring how many times M occurs as an element on N.

Notice the following:

\begin{code}

private
 ⁅-remark : (M N : 𝕄)
          β†’ (M ⁅ N) ＝ fiber (𝕄-forest N) M
 ⁅-remark M N = refl

\end{code}

In particular, if 𝕄-forest N is an embedding, then M ⁅ N holds in at
most one way. This situation is investigated in the module
Iterative.Sets.

The following fact is trivial, but it is good to have a name for it
for the sake of clarity.

\begin{code}

𝕄-forest-⁅ : (M : 𝕄) (x : 𝕄-root M) β†’ 𝕄-forest M x ⁅ M
𝕄-forest-⁅ _ x = x , refl

\end{code}

The induction principle for 𝕄, and particular cases:

\begin{code}

𝕄-induction : (P : 𝕄 β†’ π“₯ Μ‡ )
            β†’ ((X : 𝓀 Μ‡ ) (Ο† : X β†’ 𝕄)
                  β†’ ((x : X) β†’ P (Ο† x))
                  β†’ P (ssup X Ο†))
            β†’ (M : 𝕄) β†’ P M
𝕄-induction = W-induction

𝕄-recursion : (P : π“₯ Μ‡ )
            β†’ ((X : 𝓀 Μ‡ ) β†’ (X β†’ 𝕄) β†’ (X β†’ P) β†’ P)
            β†’ 𝕄 β†’ P
𝕄-recursion = W-recursion

𝕄-iteration : (P : π“₯ Μ‡ )
            β†’ ((X : 𝓀 Μ‡ ) β†’ (X β†’ P) β†’ P)
            β†’ 𝕄 β†’ P
𝕄-iteration = W-iteration

\end{code}

A criterion for equality in 𝕄:

\begin{code}

to-𝕄-＝ : {X Y : 𝓀 Μ‡ }
          {Ο† : X β†’ 𝕄}
          {Ξ³ : Y β†’ 𝕄}
        β†’ (Ξ£ p κž‰ X ＝ Y , Ο† ＝ Ξ³ ∘ Idtofun p)
        β†’ ssup X Ο† ＝[ 𝕄 ] ssup Y Ξ³
to-𝕄-＝ = to-W-＝

from-𝕄-＝ : {X Y : 𝓀 Μ‡ }
            {Ο† : X β†’ 𝕄}
            {Ξ³ : Y β†’ 𝕄}
          β†’ ssup X Ο† ＝[ 𝕄 ] ssup Y Ξ³
          β†’ Ξ£ p κž‰ X ＝ Y , Ο† ＝ Ξ³ ∘ Idtofun p
from-𝕄-＝ = from-W-＝

from-to-𝕄-＝ : {X Y : 𝓀 Μ‡ }
               {Ο† : X β†’ 𝕄}
               {Ξ³ : Y β†’ 𝕄}
               (Οƒ : Ξ£ p κž‰ X ＝ Y , Ο† ＝ Ξ³ ∘ Idtofun p)
             β†’ from-𝕄-＝ {X} {Y} {Ο†} {Ξ³} (to-𝕄-＝ Οƒ) ＝ Οƒ
from-to-𝕄-＝ = from-to-W-＝

to-from-𝕄-＝ : {X Y : 𝓀 Μ‡ }
            {Ο† : X β†’ 𝕄}
            {Ξ³ : Y β†’ 𝕄}
            (p : ssup X Ο† ＝ ssup Y Ξ³)
          β†’ to-𝕄-＝ (from-𝕄-＝ p) ＝ p
to-from-𝕄-＝ = to-from-W-＝

𝕄-＝ : {X Y : 𝓀 Μ‡ }
       {Ο† : X β†’ 𝕄}
       {Ξ³ : Y β†’ 𝕄}
     β†’ (ssup X Ο† ＝[ 𝕄 ] ssup Y Ξ³)
     ≃ (Ξ£ p κž‰ X ＝ Y , Ο† ＝ Ξ³ ∘ Idtofun p)
𝕄-＝ = W-＝

𝕄-＝' : (M N : 𝕄) β†’ (M ＝ N) ≃ (fiber ((𝕄-forest N ∘_) ∘ Idtofun) (𝕄-forest M))
𝕄-＝'  M@(ssup X Ο†) N@(ssup Y Ξ³) =
 (ssup X Ο† ＝ ssup Y Ξ³)              β‰ƒβŸ¨ 𝕄-＝ ⟩
 (Ξ£ p κž‰ X ＝ Y , Ο† ＝ Ξ³ ∘ Idtofun p) β‰ƒβŸ¨ Ξ£-cong (Ξ» p β†’ ＝-flip) ⟩
 (Ξ£ p κž‰ X ＝ Y , Ξ³ ∘ Idtofun p ＝ Ο†) β‰ƒβŸ¨ ≃-refl _ ⟩
 fiber ((Ξ³ ∘_) ∘ Idtofun) Ο†          β– 

\end{code}

The above works in pure MLTT without any HoTT/UF assumptions.

We now show that 𝕄 is locally small assuming univalence. For this
purpose, we characterize identification of multisets as follows.

TODO. Notice that there is some ammount of repetition compared with
Iterative.W-Properties. Can we avoid it by proving something more
general that subsumes both cases?

\begin{code}

_≃ᴹ_ : 𝕄 β†’ 𝕄 β†’ 𝓀 Μ‡
ssup X Ο† ≃ᴹ ssup X' Ο†' = Ξ£ 𝕗 κž‰ X ≃ X' , ((x : X) β†’ Ο† x ≃ᴹ Ο†' (⌜ 𝕗 ⌝ x))

≃ᴹ-refl : (M : 𝕄) β†’ M ≃ᴹ M
≃ᴹ-refl (ssup X Ο†) = ≃-refl X , (Ξ» x β†’ ≃ᴹ-refl (Ο† x))

singleton-typeα΄Ή : 𝕄 β†’ 𝓀⁺ Μ‡
singleton-typeα΄Ή M = Ξ£ t κž‰ 𝕄 , M ≃ᴹ t

M-center : (M : 𝕄) β†’ singleton-typeα΄Ή M
M-center M = M , ≃ᴹ-refl M

M-centrality : Univalence
             β†’ (M : 𝕄) (Οƒ : singleton-typeα΄Ή M) β†’ M-center M ＝ Οƒ
M-centrality ua (ssup X Ο†) (ssup Y Ξ³ , 𝕗 , u) =
 V (eqtoid (ua 𝓀) X Y 𝕗) (idtoeq-eqtoid (ua 𝓀) X Y 𝕗 ⁻¹)
 where
  V : (p : X ＝ Y) β†’ 𝕗 ＝ idtoeq X Y p β†’ M-center (ssup X Ο†) ＝ ssup Y Ξ³ , 𝕗 , u
  V refl refl = IV
   where
    IH : (x : X) β†’ M-center (Ο† x) ＝ Ξ³ (⌜ 𝕗 ⌝ x) , u x
    IH x = M-centrality ua (Ο† x) (Ξ³ (⌜ 𝕗 ⌝ x) , u x)

    I : (Ξ» x β†’ M-center (Ο† x)) ＝ (Ξ» x β†’ Ξ³ (⌜ 𝕗 ⌝ x) , u x)
    I = dfunext (Univalence-gives-Fun-Ext ua) IH

    Ο€ : (Ξ£ Ξ΄ κž‰ (X β†’ 𝕄) , ((x : X) β†’ Ο† x ≃ᴹ Ξ΄ x))
      β†’ singleton-typeα΄Ή (ssup X Ο†)
    Ο€ (Ξ΄ , v) = ssup X Ξ΄ , ≃-refl X , v

    II : (Ο† , Ξ» x β†’ ≃ᴹ-refl (Ο† x)) ＝ (Ξ³ ∘ ⌜ 𝕗 ⌝ , u)
    II = ap Ξ Ξ£-distr I

    III : (ssup X Ο† ,           ≃-refl X , Ξ» x β†’ ≃ᴹ-refl (Ο† x))
       ＝ (ssup X (Ξ³ ∘ ⌜ 𝕗 ⌝) , ≃-refl X , u)
    III = ap Ο€ II

    IV =
     M-center (ssup X Ο†)                         ＝⟨ refl ⟩
     ssup X Ο† , ≃-refl X , (Ξ» x β†’ ≃ᴹ-refl (Ο† x)) ＝⟨ III ⟩
     ssup X (Ξ³ ∘ ⌜ 𝕗 ⌝) , ≃-refl X , u           ＝⟨ refl ⟩
     ssup Y Ξ³ , 𝕗 , u                            ∎

singleton-typesα΄Ή-are-singletons : Univalence
                                β†’ (M : 𝕄) β†’ is-singleton (singleton-typeα΄Ή M)
singleton-typesα΄Ή-are-singletons ua M = M-center M , M-centrality ua M

idtoeqα΄Ή : (M N : 𝕄) β†’ M ＝ N β†’ M ≃ᴹ N
idtoeqα΄Ή M M refl = ≃ᴹ-refl M

idtoeqα΄Ή-is-equiv : Univalence
                 β†’ (M t : 𝕄) β†’ is-equiv (idtoeqα΄Ή M t)
idtoeqα΄Ή-is-equiv ua M = I
 where
  f : singleton-type M β†’ singleton-typeα΄Ή M
  f = NatΞ£ (idtoeqα΄Ή M)

  f-is-equiv : is-equiv f
  f-is-equiv = maps-of-singletons-are-equivs f
                (singleton-types-are-singletons M)
                (singleton-typesα΄Ή-are-singletons ua M)

  I : (t : 𝕄) β†’ is-equiv (idtoeqα΄Ή M t)
  I = NatΞ£-equiv-gives-fiberwise-equiv (idtoeqα΄Ή M) f-is-equiv

𝕄-＝-≃ : Univalence
      β†’ (M N : 𝕄) β†’ (M ＝ N) ≃ (M ≃ᴹ N)
𝕄-＝-≃ ua M N = idtoeqα΄Ή M N , idtoeqα΄Ή-is-equiv ua M N

\end{code}

And here is the desired conclusion:

\begin{code}

𝕄-is-locally-small : Univalence
                   β†’ is-locally-small 𝕄
𝕄-is-locally-small ua M N = M ≃ᴹ N , ≃-sym (𝕄-＝-≃ ua M N)

\end{code}

Not only the type of identifications of elements of 𝕄 has a small
copy, but also so does the (multi-valued) membership relation:

\begin{code}

_⁅⁻_ : 𝕄 β†’ 𝕄 β†’ 𝓀 Μ‡
M ⁅⁻ N = Ξ£ x κž‰ 𝕄-root N , 𝕄-forest N x ≃ᴹ M

⁅⁻≃⁅ : Univalence
     β†’ (M N : 𝕄) β†’ (M ⁅ N) ≃ (M ⁅⁻ N)
⁅⁻≃⁅ ua M N = Ξ£-cong (Ξ» x β†’ 𝕄-＝-≃ ua (𝕄-forest N x) M)

\end{code}