fix error

TODO.txt

@@ -8,3 +8,27 @@ talk with Favonia about:
 - higher cube filling strategies
 - HIT equivalences
 - algebra
+
+
+/-
+Adjointness:
+Σ X ⟶ Y    X ∧ Y → Z
+=======    ===========
+X → Ω Y    X → (Y → Z)
+
+Spectrum: Y : ℕ → Type* with e : Ω Yₙ₊₁ ≃* Yₙ.
+
+
+HOMOLOGY:
+Hₙ(X, Y) :≡? ∥ X ∧ Ω² (Y (n+2)) ∥₀ ≃ ∥ X ∧ Y n ∥₀
+
+Eilenberg Steenrod-axioms:
+H : ℤ → Type* → AbGroup
+- functorial in second argument
+- (optional): respects pointed equivalences and pointed homotopies
+axioms:
+- the canonical map
+-
+- Given (Xᵢ)ᵢ : I → Type* (satisfying AC?) the canonical functor
+  ⊕ hₙ
+-/

homotopy/EM.hlean

@@ -1,6 +1,6 @@
 -- Authors: Floris van Doorn
 
-import homotopy.EM algebra.category.functor.equivalence ..pointed ..pointed_pi
+import homotopy.EM algebra.category.functor.equivalence types.pointed2 ..pointed_pi ..pointed
 
 open eq equiv is_equiv algebra group nat pointed EM.ops is_trunc trunc susp function is_conn
 
@@ -617,7 +617,8 @@ namespace EM
       (trivial_homotopy_group_of_is_trunc (ptrunc 0 A) !zero_lt_succ), exact sorry
 --      rexact isomorphism_of_equiv (equiv_of_isomorphism z) sorry
       },
-    { apply @is_conn_fun_trunc_elim, apply is_conn_fun_tr }
+    { apply @is_conn_fun_trunc_elim, apply is_conn_fun_tr },
+    { apply is_trunc_pfiber }
   end
 
   definition pfiber_postnikov_map_succ (A : Type*) (n : ℕ) :

homotopy/cohomology.hlean

@@ -15,7 +15,7 @@ namespace cohomology
 
 /- The cohomology of X with coefficients in Y is
    trunc 0 (A →* Ω[2] (Y (n+2)))
-   In the file arrow_group (in algebra) we construct the group structor on this type.
+   In the file arrow_group (in algebra) we construct the group structure on this type.
 -/
 definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : AbGroup :=
 AbGroup_trunc_pmap X (Y (n+2))