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

Created on 2023-01-26.
Last modified on 2023-10-22.

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


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


The type of small multisets

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

The large type of all multisets

  Large-𝕍 : UUω
  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