The universal multiset

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

Created on 2023-01-26.
Last modified on 2023-09-11.

module trees.universal-multiset where
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


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


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


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
      ( 𝕎 U  x  pr1 (H (map-inv-equiv e x))))
      ( equiv-𝕎
        ( λ u  type-is-small (H (map-inv-equiv e u)))
        ( e)
        ( λ X 
            ( λ t  X  pr1 (H t))
            ( inv (is-retraction-map-inv-equiv e X))
            ( pr2 (H X)))))
    ( f)
    f :
      (X : 𝕍 l1) 
      is-small-𝕍 l (resize-𝕍 X (is-small-multiset-𝕍 is-small-lsuc X))
    f (tree-𝕎 A α) =
        ( 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)))

Recent changes