_≠ 0 ∘ μ

UniMath · Oct 9, 2023 · 9f9de02 · 9f9de02
1 parent 2ec50ea
commit 9f9de02
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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