Empty multisets

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-22.
Last modified on 2024-04-11.

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

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

Idea

A multiset is said to be empty if it has no elements.

Definition

The predicate of being an empty multiset

module _
  {l : Level}
  where

  is-empty-𝕍 : 𝕍 l → UU l
  is-empty-𝕍 (tree-𝕎 X Y) = is-empty X

  is-property-is-empty-𝕍 : (X : 𝕍 l) → is-prop (is-empty-𝕍 X)
  is-property-is-empty-𝕍 (tree-𝕎 X Y) = is-property-is-empty

  is-empty-prop-𝕍 : 𝕍 l → Prop l
  is-empty-prop-𝕍 X = is-empty-𝕍 X , is-property-is-empty-𝕍 X

The predicate of being a multiset with no elements

However, note that this predicate returns a type of universe level lsuc l.

module _
  {l : Level}
  where

  has-no-elements-𝕍 : 𝕍 l → UU (lsuc l)
  has-no-elements-𝕍 X = (Y : 𝕍 l) → Y ∉-𝕎 X

Properties

A multiset X is empty if and only if it has no elements

module _
  {l : Level}
  where

  is-empty-has-no-elements-𝕍 :
    (X : 𝕍 l) → has-no-elements-𝕍 X → is-empty-𝕍 X
  is-empty-has-no-elements-𝕍 (tree-𝕎 X Y) H x = H (Y x) (x , refl)

  has-no-elements-is-empty-𝕍 :
    (X : 𝕍 l) → is-empty-𝕍 X → has-no-elements-𝕍 X
  has-no-elements-is-empty-𝕍 (tree-𝕎 X Y) H ._ (x , refl) = H x

Recent changes