Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Eléonore Mangel.

Created on 2022-04-08.
Last modified on 2023-10-09.

module foundation.multisubsets where
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.images
open import foundation.negated-equality
open import foundation.universe-levels

open import foundation-core.fibers-of-maps
open import foundation-core.sets

open import univalent-combinatorics.finite-types


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


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

  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 (fiber 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}

  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  0)

  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 μ)

Recent changes