Martin Escardo and Tom de Jong, July 2023.

Some constructions with iterative multisets.

 * The universe is a retract of the type 𝕄 of iterative multisets.
 * 𝕄 is algebraically injective.

\begin{code}

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

open import MLTT.Spartan hiding (_^_)
open import UF.Sets-Properties
open import UF.Univalence
open import UF.Universes

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

open import Iterative.Multisets 𝓀
open import Iterative.Sets ua 𝓀
open import UF.Base
open import UF.DiscreteAndSeparated
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.ClassicalLogic
open import UF.FunExt
open import UF.HedbergApplications
open import UF.PropIndexedPiSigma
open import UF.Retracts
open import UF.Sets
open import UF.Size
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 Taboos.Decomposability fe'
open import InjectiveTypes.Blackboard fe'

\end{code}

The universe 𝓀 is embedded as a retract of 𝕄. This seems to be a new
observation.

\begin{code}

𝟘ᴹ : 𝕄
𝟘ᴹ = ssup 𝟘 unique-from-𝟘

𝟘ᴹ-is-iset : is-iterative-set 𝟘ᴹ
𝟘ᴹ-is-iset = unique-from-𝟘-is-embedding , (Ξ» (x : 𝟘) β†’ 𝟘-elim x)

𝟘ᴹ-is-h-isolated : is-h-isolated 𝟘ᴹ
𝟘ᴹ-is-h-isolated {ssup X Ο†} = isets-are-h-isolated 𝟘ᴹ 𝟘ᴹ-is-iset

πŸ™α΄Ή : 𝕄
πŸ™α΄Ή = ssup πŸ™ Ξ» ⋆ β†’ 𝟘ᴹ

πŸ™α΄Ή-is-iset : is-iterative-set πŸ™α΄Ή
πŸ™α΄Ή-is-iset = global-point-is-embedding (Ξ» ⋆ β†’ 𝟘ᴹ) 𝟘ᴹ-is-h-isolated ,
             Ξ» ⋆ β†’ 𝟘ᴹ-is-iset

πŸ™α΄Ή-is-h-isolated : is-h-isolated πŸ™α΄Ή
πŸ™α΄Ή-is-h-isolated {ssup X Ο†} = isets-are-h-isolated πŸ™α΄Ή πŸ™α΄Ή-is-iset

𝟘ᴹ-is-not-πŸ™α΄Ή : 𝟘ᴹ β‰  πŸ™α΄Ή
𝟘ᴹ-is-not-πŸ™α΄Ή p = 𝟘-is-not-πŸ™ (ap 𝕄-root p)

𝟚ᴹ : 𝕄
𝟚ᴹ = ssup (πŸ™ {𝓀} + πŸ™ {𝓀}) (cases (Ξ» _ β†’ 𝟘ᴹ) (Ξ» _ β†’ πŸ™α΄Ή))

universe-to-𝕄 : 𝓀 Μ‡ β†’ 𝕄
universe-to-𝕄 X = ssup X (Ξ» x β†’ 𝟘ᴹ)

universe-to-𝕄-is-section : 𝕄-root ∘ universe-to-𝕄 ∼ id
universe-to-𝕄-is-section X = refl

universe-is-retract-of-𝕄 : retract (𝓀 Μ‡ ) of 𝕄
universe-is-retract-of-𝕄 = 𝕄-root , universe-to-𝕄 , universe-to-𝕄-is-section

𝕄-is-not-set : Β¬ is-set 𝕄
𝕄-is-not-set i = universes-are-not-sets (ua 𝓀)
                  (retract-of-set universe-is-retract-of-𝕄 i)

\end{code}

Although a section is not an embedding in general, in this case it is.

\begin{code}

universe-to-𝕄-is-embedding : is-embedding universe-to-𝕄
universe-to-𝕄-is-embedding M@(ssup Y Ο†) = II
 where
  I = fiber universe-to-𝕄 M                                           β‰ƒβŸ¨ ≃-refl _ ⟩
      (Ξ£ X κž‰ 𝓀 Μ‡ , ssup X (Ξ» x β†’ 𝟘ᴹ) ＝ (ssup Y Ο†))                    β‰ƒβŸ¨ Iβ‚€ ⟩
      (Ξ£ X κž‰ 𝓀 Μ‡ , Ξ£ p κž‰ X ＝ Y , (Ξ» x β†’ 𝟘ᴹ) ＝ Ο† ∘ Idtofun p)         β‰ƒβŸ¨ I₁ ⟩
      (Ξ£ (X , p) κž‰ (Ξ£ X κž‰ 𝓀 Μ‡ , X ＝ Y) , (Ξ» x β†’ 𝟘ᴹ) ＝ Ο† ∘ Idtofun p) β– 
   where
    Iβ‚€ = Ξ£-cong (Ξ» X β†’ 𝕄-＝)
    I₁ = ≃-sym Ξ£-assoc

  II : is-prop (fiber universe-to-𝕄 M)
  II = equiv-to-prop I
        (subsets-of-props-are-props _ _
          (singleton-types'-are-props Y)
          (constant-maps-are-h-isolated fe 𝟘ᴹ 𝟘ᴹ-is-h-isolated))

\end{code}

Submultisets.

\begin{code}

𝕄-separation : (M : 𝕄) (P : 𝕄 β†’ 𝓀 Μ‡ )
             β†’ Ξ£ M' κž‰ 𝕄 , ((N : 𝕄) β†’ (N ⁅ M') ≃ (N ⁅ M Γ— P N))
𝕄-separation M@(ssup X Ο†) P = M' , Q
 where
  M' : 𝕄
  M' = ssup (Ξ£ x κž‰ X , P (Ο† x)) (Ξ» (x , p) β†’ Ο† x)

  Qβ†’ : (N : 𝕄) β†’ N ⁅ M' β†’ N ⁅ M Γ— P N
  Q→ N ((x , p) , refl) = (x , refl) , p

  Q← : (N : 𝕄) β†’ N ⁅ M Γ— P N β†’ N ⁅ M'
  Q← N ((x , refl) , p) = (x , p) , refl

  Ξ· : (N : 𝕄) β†’ Q← N ∘ Qβ†’ N ∼ id
  Ξ· N ((x , p) , refl) = refl

  Ξ΅ : (N : 𝕄) β†’ Qβ†’ N ∘ Q← N ∼ id
  Ξ΅ N ((x , refl) , p) = refl

  Q : (N : 𝕄) β†’ N ⁅ M' ≃ (N ⁅ M Γ— P N)
  Q N = qinveq (Qβ†’ N) (Q← N , Ξ· N , Ξ΅ N)

submultiset : 𝕄 β†’ (𝕄 β†’ 𝓀 Μ‡ ) β†’ 𝕄
submultiset M P = pr₁ (𝕄-separation M P)

submultiset-≃ : (M : 𝕄) (P : 𝕄 β†’ 𝓀 Μ‡ )
              β†’ (N : 𝕄) β†’ (N ⁅ submultiset M P) ≃ (N ⁅ M Γ— P N)
submultiset-≃ M P = prβ‚‚ (𝕄-separation M P)

\end{code}

The type of multisets is large, in the sense that it doesn' have a
small copy. This is proved using Russell's Paradox technique, using
separation as defined above.

\begin{code}

𝕄-is-large : is-large 𝕄
𝕄-is-large (X , 𝕗) = III
 where
  have-𝕗 : X ≃ 𝕄
  have-𝕗 = 𝕗

  _ : 𝓀 Μ‡
  _ = X

  _ : 𝓀⁺ Μ‡
  _ = 𝕄

  M : 𝕄
  M = ssup X ⌜ 𝕗 ⌝

  M-universal : (N : 𝕄) β†’ N ⁅ M
  M-universal N = ⌜ 𝕗 ⌝⁻¹ N , inverses-are-sections' 𝕗 N

  P : (N : 𝕄) β†’ 𝓀 Μ‡
  P N = Β¬ (N ⁅⁻ N)

  R : 𝕄
  R = submultiset M P

  g : (N : 𝕄) β†’ (N ⁅ R) ≃ (N ⁅ M Γ— Β¬ (N ⁅⁻ N))
  g = submultiset-≃ M P

  h : (R ⁅ R) ≃ (R ⁅⁻ R)
  h = ⁅⁻≃⁅ ua R R

  I : R ⁅⁻ R β†’ Β¬ (R ⁅⁻ R)
  I i = prβ‚‚ (⌜ g R ⌝ (⌜ h ⌝⁻¹ i))

  II : Β¬ (R ⁅⁻ R) β†’ R ⁅⁻ R
  II ν = ⌜ h ⌝ (⌜ g R ⌝⁻¹ (M-universal R , ν))

  III : 𝟘
  III = not-equivalent-to-own-negation (I , II)

\end{code}

The above is Russell's paradox adapted to multisets. But we also have
the following alternative proof:

\begin{code}

𝕄-is-large' : is-large 𝕄
𝕄-is-large' 𝕄-is-small = II
 where
  I : (𝓀 Μ‡ ) is 𝓀 small
  I = embedded-retract-is-small
       universe-is-retract-of-𝕄
       universe-to-𝕄-is-embedding
       𝕄-is-small

  II : 𝟘
  II = universes-are-large I

\end{code}

However, this proof, when expanded, is essentially the same as
that of Russell's paradox.

The type of multisets is algebraically injective, which is a new
result. We give two constructions, using Ξ£α΄Ή and Ξ α΄Ή defined below.

\begin{code}

Ξ£α΄Ή : {X : 𝓀 Μ‡ } β†’ (X β†’ 𝕄) β†’ 𝕄
Ξ£α΄Ή {X} A = ssup
            (Ξ£ x κž‰ X , 𝕄-root (A x))
            (Ξ» (x , y) β†’ 𝕄-forest (A x) y)

_+α΄Ή_ : 𝕄 β†’ 𝕄 β†’ 𝕄
M +α΄Ή N = Ξ£α΄Ή (cases (Ξ» (_ : πŸ™ {𝓀}) β†’ M) (Ξ» (_ : πŸ™ {𝓀}) β†’ N))

prop-indexed-sumα΄Ή : {X : 𝓀 Μ‡ } {A : X β†’ 𝕄}
                  β†’ is-prop X
                  β†’ (xβ‚€ : X) β†’ Ξ£α΄Ή A ＝ A xβ‚€
prop-indexed-sumα΄Ή {X} {A} i xβ‚€ = IV
 where
  𝕗 = (Ξ£ x κž‰ X , 𝕄-root (A x)) β‰ƒβŸ¨ prop-indexed-sum xβ‚€ i ⟩
      𝕄-root (A xβ‚€)            β– 

  remark : ⌜ 𝕗 ⌝ ＝ (Ξ» (x , y) β†’ transport (Ξ» - β†’ 𝕄-root (A -)) (i x xβ‚€) y)
  remark = refl

  I : ((x , y) : Ξ£ x κž‰ X , 𝕄-root (A x))
      (p : x ＝ xβ‚€)
    β†’ 𝕄-forest (A x) y ＝ 𝕄-forest (A xβ‚€) (transport (Ξ» - β†’ 𝕄-root (A -)) p y)
  I _ refl = refl

  II : ((x , y) : Ξ£ x κž‰ X , 𝕄-root (A x))
     β†’ 𝕄-forest (A x) y ＝ 𝕄-forest (A xβ‚€) (⌜ 𝕗 ⌝ (x , y))
  II (x , y) = I (x , y) (i x xβ‚€)

  III : Ξ£α΄Ή A ≃ᴹ ssup (𝕄-root (A xβ‚€)) (𝕄-forest (A xβ‚€))
  III = 𝕗 , (Ξ» Οƒ β†’ idtoeqα΄Ή _ _ (II Οƒ))

  IV = Ξ£α΄Ή A                                    ＝⟨ ⌜ 𝕄-＝-≃ ua _ _ ⌝⁻¹ III ⟩
       ssup (𝕄-root (A xβ‚€)) (𝕄-forest (A xβ‚€)) ＝⟨ 𝕄-Ξ· (A xβ‚€) ⟩
       A xβ‚€                                    ∎

𝕄-is-aflabby-Ξ£ : aflabby 𝕄 𝓀
𝕄-is-aflabby-Ξ£ P P-is-prop f = Ξ£α΄Ή f , prop-indexed-sumα΄Ή P-is-prop

𝕄-is-ainjective-Ξ£ : ainjective-type 𝕄 𝓀 𝓀
𝕄-is-ainjective-Ξ£ = aflabby-types-are-ainjective 𝕄 𝕄-is-aflabby-Ξ£

\end{code}

Notice that we use Ξ£α΄Ή (as well as Ξ ) in the following definition of Ξ α΄Ή.

\begin{code}

Ξ α΄Ή : {X : 𝓀 Μ‡ } β†’ (X β†’ 𝕄) β†’ 𝕄
Ξ α΄Ή {X} A = ssup
            (Ξ  x κž‰ X , 𝕄-root (A x))
            (Ξ» g β†’ Ξ£α΄Ή (Ξ» x β†’ 𝕄-forest (A x) (g x)))

_Γ—α΄Ή_ : 𝕄 β†’ 𝕄 β†’ 𝕄
M Γ—α΄Ή N = Ξ α΄Ή (cases (Ξ» (_ : πŸ™ {𝓀}) β†’ M) (Ξ» (_ : πŸ™ {𝓀}) β†’ N))

\end{code}

Question. Is there a function Ξ α΄Ή of the above type that satisfies the
following equation? It seems that this possible for finite X. We guess
there isn't such a function for general X, including X = β„•.

This question is answered in gist.multiset-addendum-question

\begin{code}

Question =
   {X : 𝓀 Μ‡ }
 β†’ Ξ£ Ξ α΄Ή κž‰ ((X β†’ 𝕄) β†’ 𝕄)
        , ((A : X β†’ 𝕄) β†’ Ξ α΄Ή A ＝ ssup
                                  (Ξ  x κž‰ X , 𝕄-root (A x))
                                  (Ξ» g β†’ Ξ α΄Ή (Ξ» x β†’ 𝕄-forest (A x) (g x))))
\end{code}

Here is the answer for X = 𝟚, up to equivalence:

\begin{code}

_Γ—α΄Ή'_ : 𝕄 β†’ 𝕄 β†’ 𝕄
(ssup X Ο†) Γ—α΄Ή' (ssup Y Ξ³) = ssup (X Γ— Y) (Ξ» (x , y) β†’ (Ο† x) Γ—α΄Ή' (Ξ³ y))

prop-indexed-productα΄Ή : {X : 𝓀 Μ‡ } {A : X β†’ 𝕄}
                      β†’ is-prop X
                      β†’ (xβ‚€ : X) β†’ Ξ α΄Ή A ＝ A xβ‚€
prop-indexed-productα΄Ή {X} {A} i xβ‚€ = IV
 where
  𝕗 = (Ξ  x κž‰ X , 𝕄-root (A x)) β‰ƒβŸ¨ prop-indexed-product xβ‚€ fe i ⟩
      𝕄-root (A xβ‚€)            β– 

  remark : ⌜ 𝕗 ⌝ ＝ Ξ» g β†’ g xβ‚€
  remark = refl

  I : (g : (x : X) β†’ 𝕄-root (A x))
      (x : X) (p : x ＝ xβ‚€)
    β†’ 𝕄-forest (A x) (g x) ＝ 𝕄-forest (A xβ‚€) (g xβ‚€)
  I g x refl = refl

  II : (g : (x : X) β†’ 𝕄-root (A x))
     β†’ Ξ£α΄Ή (Ξ» x β†’ 𝕄-forest (A x) (g x)) ＝ 𝕄-forest (A xβ‚€) (⌜ 𝕗 ⌝ g)
  II g = Ξ£α΄Ή (Ξ» x β†’ 𝕄-forest (A x) (g x))   ＝⟨ IIβ‚€ ⟩
         Ξ£α΄Ή (Ξ» x β†’ 𝕄-forest (A xβ‚€) (g xβ‚€)) ＝⟨ II₁ ⟩
         𝕄-forest (A xβ‚€) (g xβ‚€)            ＝⟨ refl ⟩
         𝕄-forest (A xβ‚€) (⌜ 𝕗 ⌝ g)         ∎
          where
           IIβ‚€ = ap Ξ£α΄Ή (dfunext fe (Ξ» x β†’ I g x (i x xβ‚€)))
           II₁ = prop-indexed-sumα΄Ή {X} {Ξ» x β†’ 𝕄-forest (A xβ‚€) (g xβ‚€)} i xβ‚€

  III : Ξ α΄Ή A ≃ᴹ ssup (𝕄-root (A xβ‚€)) (𝕄-forest (A xβ‚€))
  III = 𝕗 , Ξ» g β†’ idtoeqα΄Ή _ _ (II g)

  IV : Ξ α΄Ή A ＝ A xβ‚€
  IV = Ξ α΄Ή A                                   ＝⟨ ⌜ 𝕄-＝-≃ ua _ _ ⌝⁻¹ III ⟩
       ssup (𝕄-root (A xβ‚€)) (𝕄-forest (A xβ‚€)) ＝⟨ 𝕄-Ξ· (A xβ‚€) ⟩
       A xβ‚€                                   ∎

𝕄-is-aflabby-Ξ  : aflabby 𝕄 𝓀
𝕄-is-aflabby-Ξ  P P-is-prop f = Ξ α΄Ή f , prop-indexed-productα΄Ή P-is-prop

𝕄-is-ainjective-Ξ  : ainjective-type 𝕄 𝓀 𝓀
𝕄-is-ainjective-Ξ  = aflabby-types-are-ainjective 𝕄 𝕄-is-aflabby-Ξ 

𝕄-is-ainjective : ainjective-type 𝕄 𝓀 𝓀
𝕄-is-ainjective = 𝕄-is-ainjective-Ξ£

\end{code}

It follows that 𝕄 has no non-trivial decidable properties unless weak
excluded middle holds, which also seems to be a new result.

\begin{code}

decomposition-of-𝕄-gives-WEM : decomposition 𝕄 β†’ typal-WEM 𝓀
decomposition-of-𝕄-gives-WEM =
 decomposition-of-ainjective-type-gives-WEM
  (univalence-gives-propext (ua 𝓀))
  𝕄
  𝕄-is-ainjective

\end{code}