From 6e6fad5cb2080cc94d229fa26d4621845336fcfd Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Mon, 5 Jun 2017 17:09:48 -0400
Subject: [PATCH] fix error

---
 TODO.txt                  | 24 ++++++++++++++++++++++++
 homotopy/EM.hlean         |  5 +++--
 homotopy/cohomology.hlean |  2 +-
 3 files changed, 28 insertions(+), 3 deletions(-)

diff --git a/TODO.txt b/TODO.txt
index 79ce9f0..6e97c0b 100644
--- a/TODO.txt
+++ b/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ₙ
+-/
diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean
index b03c487..33acbbe 100644
--- a/homotopy/EM.hlean
+++ b/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 : ℕ) :
diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean
index e28f923..38a7e4c 100644
--- a/homotopy/cohomology.hlean
+++ b/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))