Multisets
Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.
Created on 2023-01-26.
Last modified on 2023-09-10.
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 multisets
𝕍 : (l : Level) → UU (lsuc l) 𝕍 l = 𝕎 (UU l) (λ X → X)
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
- 2023-09-10. Fredrik Bakke. Define precedence levels and associativities for all binary operators (#712).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-05-03. Egbert Rijke. Enriched directed trees and elements of W-types (#561).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497).