Multisubsets

module foundation.multisubsets where

Imports

open import elementary-number-theory.natural-numbers

open import foundation.images

open import foundation-core.dependent-pair-types
open import foundation-core.fibers-of-maps
open import foundation-core.identity-types
open import foundation-core.negation
open import foundation-core.sets
open import foundation-core.universe-levels

open import univalent-combinatorics.finite-types

Idea

A multisubset of a given set U is a type B equipped with a function f : B → U

Definition

module _
  {l1 : Level} (l2 : Level)
  where

  multisubset : Set l1 → UU (l1 ⊔ lsuc l2)
  multisubset U = Σ (UU l2) (λ B → B → type-Set U)

  is-locally-finite-multisubset :
    (U : Set l1) → multisubset U → UU (l1 ⊔ l2)
  is-locally-finite-multisubset U (pair B f) =
    (x : type-Set U) → is-finite (fib f x)

  is-finite-multisubset :
    (U : Set l1) → multisubset U → UU (l1 ⊔ l2)
  is-finite-multisubset U (pair B f) = is-finite (im f)

module _
  {l1 : Level}
  where

  locally-finite-multisubset : Set l1 → UU l1
  locally-finite-multisubset U = type-Set U → ℕ

  support-locally-finite-multisubset :
    (U : Set l1) → locally-finite-multisubset U → UU l1
  support-locally-finite-multisubset U μ =
    Σ (type-Set U) λ x → ¬ (μ x ＝ zero-ℕ)

  is-finite-locally-finite-multisubset :
    (U : Set l1) → locally-finite-multisubset U → UU l1
  is-finite-locally-finite-multisubset U μ =
    is-finite (support-locally-finite-multisubset U μ)