# Multisets

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

Created on 2023-01-26.

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)