From 9f9de02f52005e7029578a3c80e90a0fc8939b4d Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 9 Oct 2023 14:59:04 +0200 Subject: [PATCH] =?UTF-8?q?`=5F=E2=89=A0=200=20=E2=88=98=20=CE=BC`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/foundation/multisubsets.lagda.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/foundation/multisubsets.lagda.md b/src/foundation/multisubsets.lagda.md index dcf3673b6e..004d510e28 100644 --- a/src/foundation/multisubsets.lagda.md +++ b/src/foundation/multisubsets.lagda.md @@ -12,6 +12,7 @@ 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.function-types open import foundation.universe-levels open import foundation-core.fibers-of-maps @@ -56,7 +57,7 @@ module _ support-locally-finite-multisubset : (U : Set l1) → locally-finite-multisubset U → UU l1 support-locally-finite-multisubset U μ = - Σ (type-Set U) (λ x → μ x ≠ zero-ℕ) + Σ (type-Set U) (λ {≠ → precomp μ UU (_≠ 0) ≠}) is-finite-locally-finite-multisubset : (U : Set l1) → locally-finite-multisubset U → UU l1