From 3c51bbea1f8129806b97b7cd405c7987548d8480 Mon Sep 17 00:00:00 2001
From: spiceghello <stefano.piceghello@uib.no>
Date: Fri, 9 Jun 2017 10:36:10 -0600
Subject: [PATCH] minor

---
 homology/homology.hlean | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/homology/homology.hlean b/homology/homology.hlean
index e656240..3c90cd3 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -116,6 +116,17 @@ definition homology_functor [constructor] {X Y : Type*} {E F : prespectrum} (f :
   (g : E →ₛ F) (n : ℤ) : homology X E n →g homology Y F n :=
 pshomotopy_group_fun n (smash_prespectrum_fun f g)
 
+definition homology_theory_spectrum_is_exact.{u} (E : spectrum.{u}) (n : ℤ) {X Y : Type*} (f : X →* Y) :
+  is_exact_g (homology_functor f (sid (gen_spectrum.to_prespectrum E)) n)
+      (homology_functor (pcod f) (sid (gen_spectrum.to_prespectrum E)) n) :=
+begin
+  esimp[is_exact_g],
+  -- fconstructor,
+  -- { intro a, exact sorry },
+  -- { intro a, exact sorry }
+  exact sorry
+end
+
 definition homology_theory_spectrum.{u} [constructor] (E : spectrum.{u}) : homology_theory.{u} :=
 begin
   fapply homology_theory.mk,
@@ -125,7 +136,7 @@ begin
   exact sorry,
   exact sorry,
   exact sorry,
-  exact sorry,
+  apply homology_theory_spectrum_is_exact,
   exact sorry
   -- sorry
   -- sorry