# The universal multiset

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2023-01-26.

module trees.universal-multiset where

Imports
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.raising-universe-levels
open import foundation.small-types
open import foundation.small-universes
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import trees.functoriality-w-types
open import trees.multisets
open import trees.small-multisets
open import trees.w-types


## Idea

The universal multiset of universe level l is the multiset of level lsuc l built out of 𝕍 l and resizings of the multisets it contains

## Definition

universal-multiset-𝕍 : (l : Level) → 𝕍 (lsuc l)
universal-multiset-𝕍 l =
tree-𝕎
( 𝕍 l)
( λ X → resize-𝕍 X (is-small-multiset-𝕍 is-small-lsuc X))


## Properties

### If UU l1 is UU l-small, then the universal multiset of level l1 is UU l-small

is-small-universal-multiset-𝕍 :
(l : Level) {l1 : Level} →
is-small-universe l l1 → is-small-𝕍 l (universal-multiset-𝕍 l1)
is-small-universal-multiset-𝕍 l {l1} (pair (pair U e) H) =
pair
( pair
( 𝕎 U (λ x → pr1 (H (map-inv-equiv e x))))
( equiv-𝕎
( λ u → type-is-small (H (map-inv-equiv e u)))
( e)
( λ X →
tr
( λ t → X ≃ pr1 (H t))
( inv (is-retraction-map-inv-equiv e X))
( pr2 (H X)))))
( f)
where
f :
(X : 𝕍 l1) →
is-small-𝕍 l (resize-𝕍 X (is-small-multiset-𝕍 is-small-lsuc X))
f (tree-𝕎 A α) =
pair
( pair
( type-is-small (H A))
( equiv-is-small (H A) ∘e inv-equiv (compute-raise (lsuc l1) A)))
( λ x → f (α (map-inv-raise x)))