From c9ce91524f060165dbb7076140ddc16e41885cf5 Mon Sep 17 00:00:00 2001 From: favonia Date: Fri, 9 Jun 2017 06:38:07 -0600 Subject: [PATCH] Fix typo and type of Hfwedge. --- homology/homology.hlean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 :=