diff --git a/homology/homology.hlean b/homology/homology.hlean
index 00fc5d1..f220b76 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -78,7 +78,7 @@ namespace homology
       }
     end
 
-    definition Hfwehce (n : ℤ) {I : Set} (X : I → Type*): HH theory n (⋁ X) ≃g dirsum (λi, HH theory n (X i)) :=
+    definition Hfwedge (n : ℤ) {I : Type} [is_set I] (X : I → Type*): HH theory n (⋁ X) ≃g dirsum (λi, HH theory n (X i)) :=
       (isomorphism.mk _ (Hadditive theory n X))⁻¹ᵍ
 
     definition Hpwedge (n : ℤ) (A B : Type*) : HH theory n (pwedge A B) ≃g HH theory n A ×g HH theory n B :=