Multisets

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

Created on 2023-01-26.
Last modified on 2024-10-09.

module trees.multisets where
Imports 
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.function-types
open import foundation.universe-levels

open import trees.elementhood-relation-w-types
open import trees.w-types

Idea

The type of multisets of universe level l is the W-type of the universal family over the universe UU l.

Definitions

The type of small multisets

𝕍 : (l : Level) → UU (lsuc l)
𝕍 l = 𝕎 (UU l) (λ X → X)

The large type of all multisets

data
  Large-𝕍 : UUω
  where
  tree-Large-𝕍 : {l : Level} (X : UU l) → (X → Large-𝕍) → Large-𝕍

The elementhood relation on multisets

infix 6 _∈-𝕍_ _∉-𝕍_

_∈-𝕍_ : {l : Level} → 𝕍 l → 𝕍 l → UU (lsuc l)
X ∈-𝕍 Y = X ∈-𝕎 Y

_∉-𝕍_ : {l : Level} → 𝕍 l → 𝕍 l → UU (lsuc l)
X ∉-𝕍 Y = is-empty (X ∈-𝕍 Y)

Comprehension for multisets

comprehension-𝕍 :
  {l : Level} (X : 𝕍 l) (P : shape-𝕎 X → UU l) → 𝕍 l
comprehension-𝕍 X P =
  tree-𝕎 (Σ (shape-𝕎 X) P) (component-𝕎 X ∘ pr1)

Recent changes