From 1abb09b0627caf6a48f1ad9c28e20ca1eabc54f7 Mon Sep 17 00:00:00 2001
From: Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
Date: Sat, 8 Jul 2017 12:22:31 +0100
Subject: [PATCH] one sorry less:
 parametrized_cohomology_isomorphism_shomotopy_group_spi

---
 homotopy/cohomology.hlean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean
index 9949e34..fb07352 100644
--- a/homotopy/cohomology.hlean
+++ b/homotopy/cohomology.hlean
@@ -80,7 +80,13 @@ sorry /- TODO FOR SSS -/
 
 definition parametrized_cohomology_isomorphism_shomotopy_group_spi {X : Type*} (Y : X → spectrum)
   {n m : ℤ} (p : -m = n) : pH^n[(x : X), Y x] ≃g πₛ[m] (spi X Y) :=
-sorry /- TODO FOR SSS -/
+begin
+  apply isomorphism.trans (trunc_ppi_loop_isomorphism (λx, Ω (Y x (n + 2))))⁻¹ᵍ,
+  apply homotopy_group_isomorphism_of_pequiv 0, esimp,
+  have q : sub 2 m = n + 2,
+  from (int.add_comm (of_nat 2) (-m) ⬝ ap (λk, k + of_nat 2) p),
+  rewrite q, symmetry, apply ppi_loop_pequiv
+end
 
 definition unreduced_parametrized_cohomology_isomorphism_shomotopy_group_supi {X : Type}
   (Y : X → spectrum) {n m : ℤ} (p : -m = n) : upH^n[(x : X), Y x] ≃g πₛ[m] (supi X Y) :=