Bounded multisets

Content created by Egbert Rijke and Fredrik Bakke.

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

module trees.bounded-multisets where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.existential-quantification
open import foundation.propositions
open import foundation.universe-levels

open import trees.empty-multisets
open import trees.multisets
open import trees.w-types

Idea

A multiset X is said to be of natural height 0 if X has no elements, and of natural height n+1 if every element in X is of natural height n. Multisets of finite natural height are said to be naturally bounded.

Note that finite multisets, which consist of finitely many elements, each of which are finite multisets, are automatically naturally bounded. Nonfinite multisets, however, need not be naturally bounded.

We also note that there should exist a more general notion of height, in which heights are measured by upwards closed subsets of the natural numbers. This is why we speak of naturally bounded multisets here. On the other hand, every multiset is bounded in this more general sense, and this bound is unique.

Definitions

The predicate of being a multiset of natural height n

module _
  {l : Level}
  where

  is-of-natural-height-𝕍 : ℕ → 𝕍 l → UU l
  is-of-natural-height-𝕍 zero-ℕ X =
    is-empty-𝕍 X
  is-of-natural-height-𝕍 (succ-ℕ n) (tree-𝕎 X Y) =
    (x : X) → is-of-natural-height-𝕍 n (Y x)

  is-prop-is-of-natural-height-𝕍 :
    (n : ℕ) (X : 𝕍 l) → is-prop (is-of-natural-height-𝕍 n X)
  is-prop-is-of-natural-height-𝕍 zero-ℕ = is-property-is-empty-𝕍
  is-prop-is-of-natural-height-𝕍 (succ-ℕ n) (tree-𝕎 X Y) =
    is-prop-Π (λ x → is-prop-is-of-natural-height-𝕍 n (Y x))

  is-of-natural-height-prop-𝕍 : ℕ → 𝕍 l → Prop l
  is-of-natural-height-prop-𝕍 n X =
    ( is-of-natural-height-𝕍 n X , is-prop-is-of-natural-height-𝕍 n X)

Explicitly bounded multisets

An explicitly bounded multiset is a multiset of specified natural height. Note that, as we will show below, every multiset of natural height n is also a multiset of natural height n + 1, so the type of natural numbers n equipped with a proof that X is of natural height n is far from a proposition.

Explicitly-Bounded-𝕍 : (l : Level) → UU (lsuc l)
Explicitly-Bounded-𝕍 l =
  Σ (𝕍 l) (λ X → Σ ℕ (λ n → is-of-natural-height-𝕍 n X))

Bounded multisets

A bounded multiset is a multiset for which a natural bound merely exists

data
  Bounded-𝕍 (l : Level) : ℕ → UU (lsuc l)
  where
  empty-multiset-Bounded-𝕍 : Bounded-𝕍 l 0
  tree-multiset-Bounded-𝕍 :
    {n : ℕ} {X : UU l} (Y : X → Bounded-𝕍 l n) → Bounded-𝕍 l (succ-ℕ n)

Bounded-𝕍' : (l : Level) → UU (lsuc l)
Bounded-𝕍' l =
  Σ (𝕍 l) (λ X → exists ℕ (λ n → is-of-natural-height-prop-𝕍 n X))

Properties

The empty multiset is of any natural height

module _
  {l : Level}
  where

  is-of-natural-height-is-empty-𝕍 :
    (n : ℕ) (X : 𝕍 l) → is-empty-𝕍 X → is-of-natural-height-𝕍 n X
  is-of-natural-height-is-empty-𝕍 zero-ℕ X H = H
  is-of-natural-height-is-empty-𝕍 (succ-ℕ n) (tree-𝕎 X Y) H x = ex-falso (H x)

A multiset of natural height n is a multiset of natural height n + 1

module _
  {l : Level}
  where

  is-of-natural-height-succ-𝕍 :
    (n : ℕ) (X : 𝕍 l) →
    is-of-natural-height-𝕍 n X → is-of-natural-height-𝕍 (succ-ℕ n) X
  is-of-natural-height-succ-𝕍 zero-ℕ X H =
    is-of-natural-height-is-empty-𝕍 1 X H
  is-of-natural-height-succ-𝕍 (succ-ℕ n) (tree-𝕎 X Y) H x =
    is-of-natural-height-succ-𝕍 n (Y x) (H x)

Recent changes