diff --git a/Cubical/Cohomology/EilenbergMacLane/Base.agda b/Cubical/Cohomology/EilenbergMacLane/Base.agda
index c22bc28635..f0c192a445 100644
--- a/Cubical/Cohomology/EilenbergMacLane/Base.agda
+++ b/Cubical/Cohomology/EilenbergMacLane/Base.agda
@@ -8,6 +8,7 @@ open import Cubical.Homotopy.EilenbergMacLane.Properties
 open import Cubical.Homotopy.EilenbergMacLane.Order2
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Transport
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Path
@@ -308,3 +309,41 @@ fst (coHomHom∙ n f) = coHomFun∙ n f
 snd (coHomHom∙ n f) =
   makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit)
     λ g h → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl))
+
+substℕ-coHom : {A : Type ℓ} {G : AbGroup ℓ'} {n m : ℕ}
+  → (p : n ≡ m)
+  → AbGroupEquiv (coHomGr n G A) (coHomGr m G A)
+fst (substℕ-coHom {A = A} {G = G} p) =
+  substEquiv' (λ i → coHom i G A) p
+snd (substℕ-coHom {A = A} {G = G} p) =
+  makeIsGroupHom
+    λ x y →
+      J (λ m p → subst (λ i → coHom i G A) p (x +ₕ y)
+                ≡ (subst (λ i → coHom i G A) p x
+                +ₕ subst (λ i → coHom i G A) p y))
+        (transportRefl _ ∙ cong₂ _+ₕ_
+          (sym (transportRefl x)) (sym (transportRefl y))) p
+
+substℕ-coHomRed : {A : Pointed ℓ} {G : AbGroup ℓ'} {n m : ℕ}
+  → (p : n ≡ m)
+  → AbGroupEquiv (coHomRedGr n G A) (coHomRedGr m G A)
+fst (substℕ-coHomRed {A = A} {G = G} p) =
+  substEquiv' (λ i → coHomRed i G A) p
+snd (substℕ-coHomRed {A = A} {G = G} p) =
+  makeIsGroupHom
+    λ x y →
+      J (λ m p → subst (λ i → coHomRed i G A) p (x +ₕ∙ y)
+                ≡ (subst (λ i → coHomRed i G A) p x
+                +ₕ∙ subst (λ i → coHomRed i G A) p y))
+        (transportRefl _ ∙ cong₂ _+ₕ∙_
+          (sym (transportRefl x)) (sym (transportRefl y))) p
+
+subst-EM-0ₖ : ∀{ℓ} {G : AbGroup ℓ} {n m : ℕ} (p : n ≡ m)
+  → subst (EM G) p (0ₖ n) ≡ 0ₖ m
+subst-EM-0ₖ {G = G} {n = n} =
+    J (λ m p → subst (EM G) p (0ₖ n) ≡ 0ₖ m) (transportRefl _)
+
+subst-EM∙ : ∀{ℓ} {G : AbGroup ℓ} {n m : ℕ} (p : n ≡ m)
+  → EM∙ G n →∙ EM∙ G m
+fst (subst-EM∙ {G = G} p) = subst (EM G) p
+snd (subst-EM∙ p) = subst-EM-0ₖ p
diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda
index 0095ff4710..e71c8db909 100644
--- a/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda
+++ b/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda
@@ -6,8 +6,11 @@ open import Cubical.Cohomology.EilenbergMacLane.Base
 
 open import Cubical.Homotopy.EilenbergMacLane.GroupStructure
 open import Cubical.Homotopy.EilenbergMacLane.Properties
+open import Cubical.Homotopy.EilenbergMacLane.CupProduct
 open import Cubical.Homotopy.EilenbergMacLane.Base
 open import Cubical.Homotopy.Connected
+open import Cubical.Homotopy.Loopspace
+open import Cubical.Homotopy.Group.Base
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
@@ -15,12 +18,17 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Pointed.Homogeneous
 
 open import Cubical.Data.Nat renaming (_+_ to _+ℕ_)
 open import Cubical.Data.Unit
+open import Cubical.Data.Bool
+open import Cubical.Data.Sigma
 
 open import Cubical.Algebra.Group.MorphismProperties
 open import Cubical.Algebra.AbGroup.Base
+open import Cubical.Algebra.Ring
 
 open import Cubical.HITs.SetTruncation as ST
 open import Cubical.HITs.Truncation as TR
@@ -30,6 +38,9 @@ open import Cubical.HITs.Susp
 open import Cubical.HITs.Sn
 open import Cubical.HITs.S1 renaming (rec to S¹fun)
 
+open RingStr renaming (_+_ to _+r_)
+open PlusBis
+
 private
   variable
     ℓ ℓ' : Level
@@ -84,9 +95,9 @@ S¹-connElim {B = B} conA pr a ind f =
       (isConnectedPath 1 conA (f base) a .fst))
 
 module _ (G : AbGroup ℓ) where
-  open AbGroupStr (snd G)
+  open AbGroupStr (snd G) renaming (is-set to is-setG)
   H¹S¹→G : coHom 1 G S¹ → fst G
-  H¹S¹→G = ST.rec is-set λ f → ΩEM+1→EM-gen 0 (f base) (cong f loop)
+  H¹S¹→G = ST.rec is-setG λ f → ΩEM+1→EM-gen 0 (f base) (cong f loop)
 
   G→H¹S¹ : fst G → coHom 1 G S¹
   G→H¹S¹ g = ∣ S¹fun (0ₖ 1) (emloop g) ∣₂
@@ -275,3 +286,181 @@ module _ (G : AbGroup ℓ) where
                           (isConnectedEM (suc (suc n))) (0ₖ _) (f north) .fst)))
         isContrUnit*)
   snd (Hⁿ[Sᵐ⁺ⁿ,G]≅0 (suc n) m) = makeIsGroupHom λ _ _ → refl
+
+-- In fact, the above induces an equivalence (S₊∙ n →∙ EM∙ G n) ≃ G
+isSet-Sn→∙EM : (G : AbGroup ℓ) (n : ℕ) → isSet (S₊∙ n →∙ EM∙ G n)
+isSet-Sn→∙EM G n =
+  subst isSet (sym (help n)
+            ∙ isoToPath (invIso (IsoSphereMapΩ n)))
+    (AbGroupStr.is-set (snd G))
+  where
+  help : (n : ℕ) → fst ((Ω^ n) (EM∙ G n)) ≡ fst G
+  help zero = refl
+  help (suc n) =
+      cong fst (flipΩPath n)
+    ∙ cong (fst ∘ (Ω^ n))
+       (ua∙ (isoToEquiv (invIso (Iso-EM-ΩEM+1 n)))
+            (ΩEM+1→EM-refl n))
+    ∙ help n
+
+-- The equivalence (Sⁿ →∙ K(G,n)) ≃ G
+HⁿSⁿ-raw≃G : (G : AbGroup ℓ) (n : ℕ)
+  → (S₊∙ n →∙ EM∙ G n) ≃ (fst G)
+HⁿSⁿ-raw≃G G zero =
+  isoToEquiv
+    (iso (λ f → fst f false)
+         (λ g → (λ {true → _ ; false → g}) , refl)
+         (λ g → refl)
+         λ g → Σ≡Prop (λ _ → AbGroupStr.is-set (snd G) _ _)
+                       (funExt λ { false → refl ; true → sym (snd g)}))
+HⁿSⁿ-raw≃G G (suc n) =
+    compEquiv
+    (invEquiv
+      (compEquiv (fst (coHom≅coHomRed n G (S₊∙ (suc n))))
+      (isoToEquiv (setTruncIdempotentIso (isSet-Sn→∙EM G (suc n))))))
+    (fst (Hⁿ[Sⁿ,G]≅G G n))
+
+-- generator of HⁿSⁿ ≃ (Sⁿ →∙ K(G,n))
+gen-HⁿSⁿ-raw : (R : Ring ℓ) (n : ℕ)
+  → (S₊∙ n →∙ EM∙ (Ring→AbGroup  R) n)
+fst (gen-HⁿSⁿ-raw R zero) false = 1r (snd R)
+fst (gen-HⁿSⁿ-raw R zero) true = 0ₖ {G = Ring→AbGroup R} 0
+snd (gen-HⁿSⁿ-raw R zero) = refl
+fst (gen-HⁿSⁿ-raw R (suc zero)) base = 0ₖ 1
+fst (gen-HⁿSⁿ-raw R (suc zero)) (loop i) = emloop (1r (snd R)) i
+fst (gen-HⁿSⁿ-raw R (suc (suc n))) north = 0ₖ (2 +ℕ n)
+fst (gen-HⁿSⁿ-raw R (suc (suc n))) south = 0ₖ (2 +ℕ n)
+fst (gen-HⁿSⁿ-raw R (suc (suc n))) (merid a i) =
+  EM→ΩEM+1 (suc n) (gen-HⁿSⁿ-raw R (suc n) .fst a) i
+snd (gen-HⁿSⁿ-raw R (suc zero)) = refl
+snd (gen-HⁿSⁿ-raw R (suc (suc n))) = refl
+
+-- looping map (Sⁿ⁺¹ →∙ K(G,n+1)) → (Sⁿ →∙ K(G,n))
+desuspHⁿSⁿ : (G : AbGroup ℓ) (n : ℕ)
+  → (S₊∙ (suc n) →∙ EM∙ G (suc n))
+  → (S₊∙ n →∙ EM∙ G n)
+fst (desuspHⁿSⁿ G zero f) =
+  λ {false → ΩEM+1→EM-gen 0 _ (cong (fst f) loop)
+   ; true → AbGroupStr.0g (snd G)}
+fst (desuspHⁿSⁿ G (suc n) f) x =
+  ΩEM+1→EM-gen (suc n) _
+    (cong (fst f) (toSusp (S₊∙ (suc n)) x))
+snd (desuspHⁿSⁿ G zero f) = refl
+snd (desuspHⁿSⁿ G (suc n) f) =
+    cong (ΩEM+1→EM-gen (suc n) _)
+      (cong (cong (fst f)) (rCancel (merid (ptSn (suc n)))))
+  ∙ (λ i → ΩEM+1→EM-gen (suc n) _ (refl {x = snd f i}))
+  ∙ ΩEM+1→EM-refl (suc n)
+
+-- The equivalence respects desuspHⁿSⁿ
+HⁿSⁿ-raw≃G-ind : (G : AbGroup ℓ) (n : ℕ)
+  → (f : S₊∙ (suc n) →∙ EM∙ G (suc n))
+  → HⁿSⁿ-raw≃G G (suc n) .fst f
+   ≡ HⁿSⁿ-raw≃G G n .fst (desuspHⁿSⁿ G n f)
+HⁿSⁿ-raw≃G-ind G zero f = refl
+HⁿSⁿ-raw≃G-ind G (suc n) f = refl
+
+-- The equivalence preserves the unit
+gen-HⁿSⁿ-raw↦1 : (R : Ring ℓ) (n : ℕ)
+  → HⁿSⁿ-raw≃G (Ring→AbGroup R) n .fst (gen-HⁿSⁿ-raw R n) ≡ 1r (snd R)
+gen-HⁿSⁿ-raw↦1 R zero = refl
+gen-HⁿSⁿ-raw↦1 R (suc zero) = transportRefl _
+                        ∙ +IdL (snd R) (1r (snd R))
+gen-HⁿSⁿ-raw↦1 R (suc (suc n)) =
+  cong (fst (Hⁿ[Sⁿ,G]≅G (Ring→AbGroup R) n) .fst)
+      (cong ∣_∣₂ (funExt λ x
+        → (cong (ΩEM+1→EM (suc n))
+             (cong-∙ (fst (gen-HⁿSⁿ-raw R (suc (suc n))))
+               (merid x) (sym (merid (ptSn (suc n)))))
+        ∙ ΩEM+1→EM-hom (suc n) _ _)
+        ∙ cong₂ _+ₖ_
+           (Iso.leftInv (Iso-EM-ΩEM+1 (suc n))
+           (gen-HⁿSⁿ-raw R (suc n) .fst x))
+            (((λ i → ΩEM+1→EM-sym (suc n)
+              (EM→ΩEM+1 (suc n) (snd (gen-HⁿSⁿ-raw R (suc n)) i)) i)
+            ∙ cong -ₖ_ (Iso.leftInv (Iso-EM-ΩEM+1 (suc n)) (0ₖ (suc n)))
+            ∙ -0ₖ (suc n)))
+        ∙ rUnitₖ (suc n) _))
+  ∙ gen-HⁿSⁿ-raw↦1 R (suc n)
+
+-- explicit characterisation of the inverse of the equivalence
+-- in terms of ⌣ₖ.
+HⁿSⁿ-raw≃G-inv : (R : Ring ℓ) (n : ℕ)
+  → fst R → (S₊∙ n →∙ EM∙ (Ring→AbGroup R) n)
+fst (HⁿSⁿ-raw≃G-inv R n r) x =
+  subst (EM (Ring→AbGroup R)) (+'-comm n 0)
+    (_⌣ₖ_ {n = n} {m = 0} (fst (gen-HⁿSⁿ-raw R n) x) r)
+snd (HⁿSⁿ-raw≃G-inv R n r) =
+  cong (subst (EM (Ring→AbGroup R)) (+'-comm n 0))
+        (cong (_⌣ₖ r) (snd (gen-HⁿSⁿ-raw R n))
+       ∙ 0ₖ-⌣ₖ n 0 r)
+       ∙ λ j → transp (λ i → EM (Ring→AbGroup R)
+                               (+'-comm n 0 (i ∨ j)))
+                     j (0ₖ (+'-comm n 0 j))
+
+
+HⁿSⁿ-raw≃G-inv-isInv : (R : Ring ℓ) (n : ℕ) (r : fst R) →
+      ((fst (HⁿSⁿ-raw≃G (Ring→AbGroup R) n))
+     ∘ HⁿSⁿ-raw≃G-inv R n) r
+     ≡ r
+HⁿSⁿ-raw≃G-inv-isInv R zero r = transportRefl _ ∙ ·IdL (snd R) r
+HⁿSⁿ-raw≃G-inv-isInv R (suc zero) r =
+    transportRefl _
+  ∙ transportRefl _
+  ∙ cong₂ (_+r_ (snd R)) (transportRefl (0r (snd R)))
+                         (transportRefl _
+                       ∙ ·IdL (snd R) r)
+  ∙ +IdL (snd R) r
+HⁿSⁿ-raw≃G-inv-isInv R (suc (suc n)) r =
+    HⁿSⁿ-raw≃G-ind (Ring→AbGroup R) (suc n) _ ∙
+    (cong (fst (HⁿSⁿ-raw≃G (Ring→AbGroup R) (suc n)))
+          (→∙Homogeneous≡
+            (isHomogeneousEM _)
+            (funExt λ z →
+              cong (ΩEM+1→EM (suc n)) (lem z)
+            ∙ Iso-EM-ΩEM+1 (suc n) .Iso.leftInv (subst (EM (Ring→AbGroup R))
+              (+'-comm (suc n) 0) (_⌣ₖ_ {m = 0}
+                (fst (gen-HⁿSⁿ-raw R (suc n)) z) r)))))
+  ∙ HⁿSⁿ-raw≃G-inv-isInv R (suc n) r
+  where
+  lem : (z : _)
+    → (λ i → subst (EM (Ring→AbGroup R)) (+'-comm (suc (suc n)) 0)
+         (fst (gen-HⁿSⁿ-raw R (suc (suc n))) (toSusp (S₊∙ (suc n)) z i) ⌣ₖ r))
+         ≡ EM→ΩEM+1 (suc n) (subst (EM (Ring→AbGroup R))
+            (+'-comm (suc n) 0)
+              (_⌣ₖ_ {m = 0} (fst (gen-HⁿSⁿ-raw R (suc n)) z) r))
+  lem z = ((λ j → transp (λ i → typ (Ω (EM∙ (Ring→AbGroup R)
+                          (+'-comm (suc (suc n)) 0 (~ j ∨ i))))) (~ j)
+            λ i → transp (λ i → EM (Ring→AbGroup R)
+                          (+'-comm (suc (suc n)) 0 (~ j ∧ i)))
+                          j
+                          (fst (gen-HⁿSⁿ-raw R (suc (suc n)))
+                           (toSusp (S₊∙ (suc n)) z i) ⌣ₖ r))
+         ∙ (λ j → transport (λ i → typ (Ω (EM∙ (Ring→AbGroup R)
+                    (isSetℕ (suc (suc n)) (suc (suc n))
+                      (+'-comm (suc (suc n)) 0) refl j i))))
+                    λ i → _⌣ₖ_ {n = suc (suc n)} {m = zero}
+                           (fst (gen-HⁿSⁿ-raw R (suc (suc n)))
+                            (toSusp (S₊∙ (suc n)) z i)) r)
+         ∙ transportRefl _
+         ∙ cong (cong (λ x → _⌣ₖ_ {n = suc (suc n)} {m = zero} x r))
+                (cong-∙ (fst (gen-HⁿSⁿ-raw R (suc (suc n))))
+                  (merid z) (sym (merid (ptSn (suc n))))
+              ∙ cong₂ _∙_ refl
+                 (cong sym (cong (EM→ΩEM+1 (suc n))
+                           (gen-HⁿSⁿ-raw R (suc n) .snd)
+                       ∙ EM→ΩEM+1-0ₖ (suc n)))
+              ∙ sym (rUnit _))
+         ∙ sym (EM→ΩEM+1-distr⌣ₖ0 n (gen-HⁿSⁿ-raw R (suc n) .fst z) r))
+        ∙ cong (EM→ΩEM+1 (suc n))
+           (sym (transportRefl _)
+          ∙ λ i → subst (EM (Ring→AbGroup R))
+                   (isSetℕ (suc n) (suc n) refl (+'-comm (suc n) 0) i)
+                   (_⌣ₖ_ {m = 0} (fst (gen-HⁿSⁿ-raw R (suc n)) z) r))
+
+-- Main lemma: HⁿSⁿ-raw≃G-inv (i.e. ⌣ₖ is an equivalence)
+isEquiv-HⁿSⁿ-raw≃G-inv : (R : Ring ℓ) (n : ℕ)
+  → isEquiv (HⁿSⁿ-raw≃G-inv R n)
+isEquiv-HⁿSⁿ-raw≃G-inv R n =
+  composesToId→Equiv _ _ (funExt (HⁿSⁿ-raw≃G-inv-isInv R n))
+    (HⁿSⁿ-raw≃G (Ring→AbGroup R) n .snd)
diff --git a/Cubical/Cohomology/EilenbergMacLane/Gysin.agda b/Cubical/Cohomology/EilenbergMacLane/Gysin.agda
new file mode 100644
index 0000000000..61c95b81e6
--- /dev/null
+++ b/Cubical/Cohomology/EilenbergMacLane/Gysin.agda
@@ -0,0 +1,1086 @@
+{-# OPTIONS --safe --lossy-unification #-}
+
+{-
+This file contains
+1. The Thom isomorphism (various related forms of it)
+2. The Gysin sequence
+-}
+
+module Cubical.Cohomology.EilenbergMacLane.Gysin where
+
+open import Cubical.Cohomology.EilenbergMacLane.Base
+open import Cubical.Cohomology.EilenbergMacLane.Groups.Sn
+open import Cubical.Cohomology.EilenbergMacLane.CupProduct
+
+open import Cubical.Homotopy.EilenbergMacLane.CupProduct
+open import Cubical.Homotopy.EilenbergMacLane.CupProductTensor
+  renaming (_⌣ₖ_ to _⌣ₖ⊗_ ; ⌣ₖ-0ₖ to ⌣ₖ-0ₖ⊗ ; 0ₖ-⌣ₖ to 0ₖ-⌣ₖ⊗)
+open import Cubical.Homotopy.Connected
+open import Cubical.Homotopy.EilenbergMacLane.GradedCommTensor
+  hiding (⌣ₖ-comm)
+open import Cubical.Homotopy.EilenbergMacLane.GroupStructure
+open import Cubical.Homotopy.EilenbergMacLane.Base
+open import Cubical.Homotopy.EilenbergMacLane.Properties
+open import Cubical.Homotopy.Loopspace
+open import Cubical.Homotopy.Group.Base
+
+open import Cubical.Functions.Morphism
+open import Cubical.Functions.Embedding
+open import Cubical.Functions.Surjection
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Transport
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Pointed.Homogeneous
+open import Cubical.Foundations.Isomorphism
+
+open import Cubical.HITs.PropositionalTruncation as PT
+open import Cubical.HITs.SetTruncation as ST
+open import Cubical.HITs.Truncation as TR
+open import Cubical.HITs.Sn
+open import Cubical.HITs.Pushout
+open import Cubical.HITs.EilenbergMacLane1.Base
+open import Cubical.HITs.Susp
+open import Cubical.HITs.S1
+
+open import Cubical.Data.Unit
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order hiding (eq)
+open import Cubical.Data.Sigma
+open import Cubical.Data.Bool hiding (_≤_)
+
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.AbGroup.Base
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Ring
+open import Cubical.Algebra.CommRing
+
+open RingStr renaming (_+_ to _+r_)
+open PlusBis
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+-- We show that a specific cup product is an
+-- equivalence. This will induce the Thom isomorphism.
+module ⌣Eq (R' : CommRing ℓ'') where
+  R = CommRing→Ring R'
+  RR = (CommRing→AbGroup R')
+  EMR = EM (CommRing→AbGroup R')
+  EMR∙ = EM∙ (CommRing→AbGroup R')
+
+  -- current goal: show that the following map is an equivalence
+  pre-g : (n i : ℕ) → EMR i → S₊∙ n →∙ EMR∙ (i +' n)
+  fst (pre-g n i x) y = x ⌣ₖ gen-HⁿSⁿ-raw R n .fst y
+  snd (pre-g n i x) =
+    cong (x ⌣ₖ_) (gen-HⁿSⁿ-raw R n .snd)
+      ∙ ⌣ₖ-0ₖ i n x
+
+
+  -- We introduce some alternative versions of the map that
+  -- may be easier to work with in some situations.
+  g-comm : (n i : ℕ) → EMR i → S₊∙ n →∙ EMR∙ (n +' i)
+  fst (g-comm n i x) y = gen-HⁿSⁿ-raw R n .fst y ⌣ₖ x
+  snd (g-comm n i x) =
+      cong (_⌣ₖ x) (gen-HⁿSⁿ-raw R n .snd)
+    ∙ 0ₖ-⌣ₖ n i x
+
+  g-cute : (n i : ℕ) → EMR i → S₊∙ n →∙ EMR∙ (i + n)
+  g-cute n i x = (subst EMR (+'≡+ i n)
+                , subst-EM-0ₖ (+'≡+ i n)) ∘∙ pre-g n i x
+
+  indexIso₁ : (n i : ℕ) → EMR∙ (i + n) ≃∙ EMR∙ (n + i)
+  fst (indexIso₁ n i) = substEquiv EMR (+-comm i n)
+  snd (indexIso₁ n i) = subst-EM-0ₖ (+-comm i n)
+
+  indexIso₂ : (n i : ℕ) → EMR∙ (n + i) ≃∙ EMR∙ (n +' i)
+  fst (indexIso₂ n i) = substEquiv EMR (sym (+'≡+ n i))
+  snd (indexIso₂ n i) = subst-EM-0ₖ (sym (+'≡+ n i))
+
+  -ₖ^-iso : ∀ {ℓ} {G : AbGroup ℓ} {k : ℕ} (n m : ℕ) → Iso (EM G k) (EM G k)
+  Iso.fun (-ₖ^-iso n m) = -ₖ^[ n · m ]
+  Iso.inv (-ₖ^-iso n m) = -ₖ^[ n · m ]
+  Iso.rightInv (-ₖ^-iso n m) = -ₖ^< n · m >² _ _ _
+  Iso.leftInv (-ₖ^-iso n m) = -ₖ^< n · m >² _ _ _
+
+  g-cute' : (n i : ℕ) → EMR i → S₊∙ n →∙ EMR∙ (n +' i)
+  g-cute' n i =
+      Iso.fun (pre∘∙equiv
+                (compEquiv∙ (isoToEquiv (-ₖ^-iso i n) , -ₖ^<_·_>∙ i n _ _ _)
+                (compEquiv∙ (indexIso₁ n i) (indexIso₂ n i))))
+    ∘ g-cute n i
+
+  g-cute≡ : (n i : ℕ) → g-cute' n i ≡ g-comm n i
+  g-cute≡ n i = funExt (λ x → →∙Homogeneous≡ (isHomogeneousEM (n +' i))
+    (funExt λ y
+      → cong (subst EMR (sym (+'≡+ n i)))
+         (cong (subst EMR (+-comm i n))
+           ((cong (-ₖ^[ i · n ])
+               (cong (subst EMR (+'≡+ i n))
+                 (⌣ₖ-comm {G'' = R'} i n x (gen-HⁿSⁿ-raw R n .fst y))))))
+      ∙ killTransp EMR -ₖ^[ i · n ] _
+         (λ _ x → -ₖ^< i · n >² _ _ _ x) _
+         (+'-comm n i)  _ _ _ _ _
+         (gen-HⁿSⁿ-raw R n .fst y ⌣ₖ x)))
+    where
+    killTransp : (A : ℕ → Type ℓ) (-ₖ_ : {n : ℕ} → A n → A n) (a : ℕ)
+      → ((n : ℕ) → (x : A n) → -ₖ (-ₖ x) ≡ x)
+      → (b : ℕ)
+      → (p : a ≡ b) (c : ℕ) (q : b ≡ c) (d : ℕ) (r : c ≡ d) (s : d ≡ a)
+      → (base : A a)
+      → subst A s (subst A r (-ₖ subst A q (subst A p (-ₖ base)))) ≡ base
+    killTransp A f i a = J> (J> (J> λ p b
+      → cong (subst A p)
+              (transportRefl _ ∙ cong f (transportRefl _ ∙ transportRefl _)
+         ∙ a _ b)
+      ∙ (λ i → subst A (isSetℕ _ _ p refl i) b)
+      ∙ transportRefl b))
+
+  isEquivBiImpl : (n i : ℕ)
+    → (isEquiv (g-comm n i) → isEquiv (g-cute n i))
+     × (isEquiv (g-cute n i) → isEquiv (g-comm n i))
+  fst (isEquivBiImpl n i) eq =
+    subst isEquiv
+      (funExt (λ x → secEq e (g-cute n i x)))
+    (compEquiv  (_ , subst isEquiv (sym (g-cute≡ n i)) eq) e .snd)
+    where
+    e = isoToEquiv (invIso (pre∘∙equiv
+                (compEquiv∙ (isoToEquiv (-ₖ^-iso i n) , -ₖ^<_·_>∙ i n _ _ _)
+                (compEquiv∙ (indexIso₁ n i) (indexIso₂ n i)))))
+  snd (isEquivBiImpl n i) eq =
+    subst isEquiv (g-cute≡ n i)
+      (compEquiv
+        (_ , eq)
+        (isoToEquiv (pre∘∙equiv
+        (compEquiv∙ (isoToEquiv (-ₖ^-iso i n) , -ₖ^<_·_>∙ i n _ _ _)
+        (compEquiv∙ (indexIso₁ n i) (indexIso₂ n i))))) .snd)
+
+  isEquiv-lem : (n i : ℕ)
+    → isEquiv (cong {x = 0ₖ (suc i)} {y = 0ₖ (suc i)}
+               (g-cute n (suc i)))
+    → (x y : EMR (suc i))
+    → isEquiv (cong {x = x} {y = y} (g-cute n (suc i)))
+  isEquiv-lem n i p =
+    EM→Prop (Ring→AbGroup R) i (λ _ → isPropΠ λ _ → isPropIsEquiv _)
+      (EM→Prop (Ring→AbGroup R) i (λ _ → isPropIsEquiv _)
+        p)
+
+  ΩFunIso : (n i : ℕ) (f : S₊∙ n →∙ EMR∙ (suc (i + n)))
+     → Iso (f ≡ f)
+            (S₊∙ n →∙ EMR∙ (i + n))
+  fst (Iso.fun (ΩFunIso n i f) st) x =
+    ΩEM+1→EM-gen (i + n) _ (funExt⁻ (cong fst st) x)
+  snd (Iso.fun (ΩFunIso n i f) st) =
+      (λ j → ΩEM+1→EM-gen (i + n) (snd f j) λ i → snd (st i) j)
+    ∙ ΩEM+1→EM-gen-refl (i + n) _
+  Iso.inv (ΩFunIso n i f) st =
+    ΣPathP ((funExt (λ x → EM→ΩEM+1-gen _ (fst f x) (fst st x)))
+           , flipSquare ((λ j → EM→ΩEM+1-gen (i + n) (snd f j) (snd st j))
+                       ▷ (EM→ΩEM+1-gen-0ₖ (i + n) _
+                       ∙ EM→ΩEM+1-0ₖ (i + n))))
+  Iso.rightInv (ΩFunIso n i f) st =
+    →∙Homogeneous≡ (isHomogeneousEM _)
+      (funExt λ x
+        → Iso.leftInv (Iso-EM-ΩEM+1-gen (i + n) (fst f x)) (st .fst x))
+  Iso.leftInv (ΩFunIso n i f) st =
+    →∙HomogeneousSquare (isHomogeneousEM _)
+      refl refl (Iso.inv (ΩFunIso n i f)
+      (Iso.fun (ΩFunIso n i f) st)) st
+      (cong funExt (funExt
+        λ x → Iso.rightInv
+          (Iso-EM-ΩEM+1-gen (i + n) (fst f x)) λ i → st i .fst x))
+
+  g-cute-ind : (n i : ℕ)
+    → g-cute n i
+    ≡ Iso.fun (ΩFunIso n i (g-cute n (suc i) (0ₖ (suc i))))
+     ∘ cong {x = 0ₖ (suc i)} {y = 0ₖ (suc i)} (g-cute n (suc i))
+     ∘ EM→ΩEM+1 i
+  g-cute-ind zero zero =
+    funExt λ x → →∙Homogeneous≡ (isHomogeneousEM {G = Ring→AbGroup R} 0)
+      (funExt λ y → transportRefl _
+        ∙ sym ((λ j → ΩEM+1→EM 0
+               (λ i → transportRefl (_⌣ₖ_ {n = 1} {m = 0}
+                       (EM→ΩEM+1 0 x i)
+                       (gen-HⁿSⁿ-raw R zero .fst y)) j))
+             ∙ Iso.leftInv (Iso-EM-ΩEM+1 0)
+                (_⌣ₖ_ {n = 0} {m = 0} x (gen-HⁿSⁿ-raw R zero .fst y))))
+  g-cute-ind zero (suc i) =
+    funExt λ x → →∙Homogeneous≡ (isHomogeneousEM _)
+      (funExt λ y →
+        sym (cong (ΩEM+1→EM (suc i + zero))
+        (cong (cong (subst EMR (cong suc (+'≡+ (suc i) zero))))
+          (sym (EM→ΩEM+1-distr⌣ₖ0 i x (gen-HⁿSⁿ-raw R zero .fst y))))
+    ∙∙ (λ j → transp (λ s → EMR (+'≡+ (suc i) zero (s ∨ ~ j))) (~ j)
+                (ΩEM+1→EM (+'≡+ (suc i) zero (~ j))
+                  λ k → transp (λ s → EMR (suc (+'≡+ (suc i) zero (s ∧ ~ j))))
+                    j
+                    (EM→ΩEM+1 (suc i) (_⌣ₖ_ {n = suc i} {m = zero}
+                      x (gen-HⁿSⁿ-raw R zero .fst y)) k)))
+    ∙∙ cong (subst EMR (λ i₁ → suc (+-zero i (~ i₁))))
+        (Iso.leftInv (Iso-EM-ΩEM+1 (suc i)) _)))
+  g-cute-ind (suc n) zero = funExt λ x → →∙Homogeneous≡ (isHomogeneousEM _)
+      (funExt λ y
+      → transportRefl _
+      ∙ sym (cong (ΩEM+1→EM (suc n))
+        ((λ k j → subst EMR (+'≡+ (suc zero) (suc n))
+          (sym (EM→ΩEM+1-distr⌣ₖ0n n x
+            (gen-HⁿSⁿ-raw R (suc n) .fst y)) k j))
+      ∙ (λ j → transp (λ i → Ω (EMR∙ (+'≡+ (suc zero) (suc n) (i ∨ j))) .fst)
+                      (~ j)
+                λ k → transp (λ i → EMR (+'≡+ (suc zero) (suc n) (i ∨ ~ j)))
+                  j (EM→ΩEM+1 (suc n)
+                    (x ⌣[ R , 0 , (suc n) ]ₖ gen-HⁿSⁿ-raw R (suc n) .fst y) k))
+      ∙ (λ j → subst (λ n → Ω (EMR∙ n) .fst)
+                 (isSetℕ (suc (suc n)) (suc (suc n))
+                   (+'≡+ (suc zero) (suc n)) refl j)
+                  (EM→ΩEM+1 (suc n)
+                    (x ⌣[ R , 0 , (suc n) ]ₖ gen-HⁿSⁿ-raw R (suc n) .fst y)))
+      ∙ transportRefl _)
+     ∙ Iso.leftInv (Iso-EM-ΩEM+1 (suc n)) _))
+  g-cute-ind (suc n) (suc i) =
+    funExt λ x → →∙Homogeneous≡ (isHomogeneousEM _)
+      (funExt λ y
+      → sym ((cong (ΩEM+1→EM (suc i + suc n)))
+               (cong (cong (subst EMR (+'≡+ (suc (suc i)) (suc n))))
+                 (sym (EM→ΩEM+1-distr⌣ₖ i n x (gen-HⁿSⁿ-raw R (suc n) .fst y))))
+           ∙ (λ j → transp (λ s → EMR (suc (+-suc i n (j ∧ ~ s)))) (~ j)
+                  ((ΩEM+1→EM (suc (+-suc i n j))
+                    (λ k → transp (λ s → EMR (suc (suc (+-suc i n (~ s ∨ j)))))
+                      j (EM→ΩEM+1 (suc (suc (i + n)))
+                       (x ⌣ₖ gen-HⁿSⁿ-raw R (suc n) .fst y) k)))))
+           ∙ cong (subst EMR (λ i₁ → suc (+-suc i n (~ i₁))))
+              (Iso.leftInv (Iso-EM-ΩEM+1 (suc i +' suc n))
+                (x ⌣ₖ gen-HⁿSⁿ-raw R (suc n) .fst y))))
+
+  g-ind-main : (n i : ℕ)
+    → isEquiv (g-cute n i) → isEquiv (g-cute n (suc i))
+  g-ind-main n i eq =
+    isEmbedding×isSurjection→isEquiv
+      ((λ x y → isEquiv-lem n i
+                  (subst isEquiv (sym help)
+                    (myEq .snd))
+                  x y)
+      , λ f → PT.map
+          (λ p → subst (fiber (g-cute n (suc i))) (sym p)
+            ((0ₖ (suc i)) , (→∙Homogeneous≡ (isHomogeneousEM _)
+              (funExt λ x → cong (subst EMR (+'≡+ (suc i) n))
+                              (0ₖ-⌣ₖ (suc i) n (gen-HⁿSⁿ-raw R n .fst x))
+                           ∙ subst-EM-0ₖ (+'≡+ (suc i) n)))))
+          (Iso.fun PathIdTrunc₀Iso
+            (isContr→isProp (help2 i n) ∣ f ∣₂ (0ₕ∙ _))))
+    where
+    myEq = compEquiv (isoToEquiv (invIso (Iso-EM-ΩEM+1 i)))
+             (compEquiv (g-cute n i , eq)
+               (isoToEquiv
+                (invIso (ΩFunIso n i (g-cute n (suc i) (0ₖ (suc i)))))))
+
+    help : cong (g-cute n (suc i))
+         ≡ myEq .fst
+    help = funExt
+      (λ p → sym
+        (Iso.leftInv (ΩFunIso n i (g-cute n (suc i) (0ₖ (suc i)))) _
+                        ∙ cong (cong (g-cute n (suc i)))
+                           (Iso.rightInv (Iso-EM-ΩEM+1 i) _)))
+         ∙ sym (cong
+            (λ f → Iso.inv (ΩFunIso n i (g-cute n (suc i) (0ₖ (suc i))))
+                     ∘ f ∘ ΩEM+1→EM i)
+               (g-cute-ind n i))
+
+    help2 : (i n : ℕ) → isContr (∥ S₊∙ n →∙ EMR∙ (suc (i + n)) ∥₂)
+    help2 i zero = 0ₕ∙ _
+      , ST.elim
+          (λ _ → isSetPathImplicit)
+          λ f → TR.rec (isProp→isOfHLevelSuc (i + zero) (squash₂ _ _))
+            (λ p → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM _)
+              (funExt λ { false → sym p ; true → sym (snd f)})))
+            (Iso.fun (PathIdTruncIso _)
+             (isContr→isProp (isConnectedEM (suc (i + zero)))
+               ∣ fst f false ∣ ∣ (0ₖ _) ∣))
+    help2 i (suc n) =
+      isOfHLevelRetractFromIso 0
+        (equivToIso (compEquiv
+          (invEquiv
+            (coHom≅coHomRed _ (Ring→AbGroup R) (S₊∙ (suc n)) .fst))
+          (fst (Hᵐ⁺ⁿ[Sⁿ,G]≅0 (Ring→AbGroup R) n i))))
+        isContrUnit*
+
+  g-cute-equiv : (i n : ℕ) → isEquiv (g-cute n i)
+  g-cute-equiv zero n = isEquivBiImpl n zero .fst
+    (subst isEquiv (sym pth)
+      (snd alt-eq))
+    where
+    alt-eq : EMR zero ≃ (S₊∙ n →∙ EMR∙ (n +' zero))
+    alt-eq = compEquiv (HⁿSⁿ-raw≃G-inv R n , isEquiv-HⁿSⁿ-raw≃G-inv R n)
+              (isoToEquiv (pre∘∙equiv
+              (substEquiv EMR (sym (+'-comm n zero)) , subst-EM-0ₖ _)))
+    pth : g-comm n zero ≡ alt-eq .fst
+    pth = funExt (λ r → →∙Homogeneous≡ (isHomogeneousEM _)
+           (funExt λ x → sym (subst⁻Subst EMR (+'-comm n zero)
+             (gen-HⁿSⁿ-raw R n .fst x ⌣ₖ r))))
+  g-cute-equiv (suc i) n = g-ind-main n i (g-cute-equiv i n)
+
+  -- main lemma
+  g-equiv : (n i : ℕ) → isEquiv (pre-g n i)
+  g-equiv n i = subst isEquiv pth (snd help)
+    where
+    help : EMR i ≃ (S₊∙ n) →∙ EMR∙ (i +' n)
+    help = compEquiv (_ , g-cute-equiv i n)
+            (isoToEquiv
+              (pre∘∙equiv
+                (substEquiv EMR (sym (+'≡+ i n))
+                , subst-EM-0ₖ (sym (+'≡+ i n)))))
+
+    pth : fst help ≡ pre-g n i
+    pth = funExt (λ r → →∙Homogeneous≡ (isHomogeneousEM _)
+            (funExt λ y
+              → subst⁻Subst EMR (+'≡+ i n)
+                  (r ⌣ₖ gen-HⁿSⁿ-raw R n .fst y)))
+
+-- We may use the above to construct the (generalised) Thom
+-- isomorphism (over a fibration with 0-connected base space)
+module preThom
+  (B : Pointed ℓ)
+  (Q : fst B → Pointed ℓ')
+  (conB : isConnected 2 (fst B))
+  (R : CommRing ℓ'')
+  (n : ℕ)
+  (e : Q (snd B) ≃∙ S₊∙ n)
+  (c : (b : fst B) → Q b →∙ EM∙ (CommRing→AbGroup R) n)
+  (r : c (pt B) ≡ (gen-HⁿSⁿ-raw (CommRing→Ring R) n ∘∙ ≃∙map e))
+  where
+  RR = (CommRing→AbGroup R)
+  EMR = EM RR
+  EMR∙ = EM∙ RR
+
+  -- Generalisation of previous map g
+  g : (i : ℕ) (b : fst B) → EMR i → Q b →∙ EMR∙ (i +' n)
+  fst (g i b x) y = x ⌣ₖ c b .fst y
+  snd (g i b x) =
+    cong (x ⌣ₖ_) (c b .snd)
+    ∙ ⌣ₖ-0ₖ i n x
+
+  isEquiv-g-pt : (i : ℕ) → isEquiv (g i (pt B))
+  isEquiv-g-pt i = subst isEquiv (sym help)  (eq .snd)
+    where
+    eq : EMR i ≃ (Q (pt B) →∙ EMR∙ (i +' n))
+    eq = compEquiv (⌣Eq.pre-g R n i , ⌣Eq.g-equiv R n i)
+                   (isoToEquiv (post∘∙equiv (invEquiv∙ e))) --
+
+    help : g i (pt B) ≡ fst eq
+    help = funExt λ x → →∙Homogeneous≡ (isHomogeneousEM _)
+             (funExt λ y → cong (λ y → x ⌣[ R , i , n ]Cₖ y)
+               (funExt⁻ (cong fst r) y))
+
+  abstract
+    isEquiv-g : (i : ℕ) (b : fst B) → isEquiv (g i b)
+    isEquiv-g i = Iso.inv (elim.isIsoPrecompose
+         (λ (x : Unit) → pt B) 1 (λ b → isEquiv (g i b) , isPropIsEquiv _)
+         (isConnectedPoint 1 conB (pt B)))
+         λ _ → isEquiv-g-pt i
+
+  g-equiv : (i : ℕ) (b : fst B) → EMR i ≃ Q b →∙ EMR∙ (i +' n)
+  g-equiv i b = g i b , isEquiv-g i b
+
+  g⁻ : (i : ℕ) (b : fst B) → Q b →∙ EMR∙ (i +' n) → EMR i
+  g⁻ i b = invEq (g-equiv i b)
+
+  private
+    g-pres+' : (i : ℕ) (b : fst B) (x y : EMR i) (z : _)
+             → g i b (x +ₖ y) .fst z ≡ (g i b x +ₖ∙ g i b y) .fst z
+    g-pres+' i b x y z =
+      distrR⌣ₖ {G'' = CommRing→Ring R} i n x y (c b .fst z)
+
+  g-pres+ : (i : ℕ) (b : fst B) (x y : EMR i)
+             → g i b (x +ₖ y) ≡ g i b x +ₖ∙ g i b y
+  g-pres+ i b x y = →∙Homogeneous≡ (isHomogeneousEM (i +' n))
+    (funExt (g-pres+' i b x y))
+
+  g⁻-pres+ : (i : ℕ) (b : fst B) (x y : _)
+    → g⁻ i b (x +ₖ∙ y) ≡ g⁻ i b x +ₖ g⁻ i b y
+  g⁻-pres+ i b =
+    morphLemmas.isMorphInv _+ₖ_ _+ₖ∙_
+      (g i b)
+      (g-pres+ i b)
+      (g⁻ i b)
+      (secEq (g-equiv i b))
+      (retEq (g-equiv i b))
+
+  pre-ϕ : (i : ℕ) → (fst B → EMR i) → (b : fst B) → Q b →∙ EMR∙ (i +' n)
+  fst (pre-ϕ i β b) x = β b ⌣ₖ c b .fst x
+  snd (pre-ϕ i β b) = cong (β b ⌣ₖ_) (c b .snd)
+                    ∙ ⌣ₖ-0ₖ i n (β b)
+
+  -- main results
+  pre-ϕIso : (i : ℕ)
+    → Iso (fst B → EMR i) ((b : fst B) → Q b →∙ EMR∙ (i +' n))
+  Iso.fun (pre-ϕIso i) = pre-ϕ i
+  Iso.inv (pre-ϕIso i) r b = invEq (g-equiv i b) (r b)
+  Iso.rightInv (pre-ϕIso i) t j b = secEq (g-equiv i b) (t b) j
+  Iso.leftInv (pre-ϕIso i) t j b = retEq (g-equiv i b) (t b) j
+
+  pre-ϕ-pres+ : (i : ℕ) → (f g : fst B → EMR i)
+    → pre-ϕ i (λ b → f b +ₖ g b) ≡ λ b → pre-ϕ i f b +ₖ∙ pre-ϕ i g b
+  pre-ϕ-pres+ i f g = funExt (λ b → →∙Homogeneous≡ (isHomogeneousEM _)
+    (funExt (g-pres+' i b (f b) (g b))))
+
+  pre-ϕ⁻-pres+ : (i : ℕ) (f g : (b : fst B) → Q b →∙ EMR∙ (i +' n))
+    → Iso.inv (pre-ϕIso i) (λ b → f b +ₖ∙ g b)
+    ≡ λ b → (Iso.inv (pre-ϕIso i) f b) +ₖ (Iso.inv (pre-ϕIso i) g b)
+  pre-ϕ⁻-pres+ i f g = funExt (λ b → g⁻-pres+ i b (f b) (g b))
+
+  isEq-ϕ : (i : ℕ) → isEquiv (pre-ϕ i)
+  isEq-ϕ i = isoToIsEquiv (pre-ϕIso i)
+
+-- The (generalised) Thom isomorphism for a fibration with a simply
+-- connected base space.
+module genThom (B : Pointed ℓ)
+         (Q : fst B → Pointed ℓ')
+         (conB : isConnected 3 (fst B))
+         (R : CommRing ℓ'')
+         (n : ℕ)
+         (e : Q (snd B) ≃∙ S₊∙ n) where
+  private
+    RR = (CommRing→AbGroup R)
+    EMR = EM RR
+    EMR∙ = EM∙ RR
+
+  Q*→EM : Q (pt B) →∙ EMR∙ n
+  Q*→EM = gen-HⁿSⁿ-raw (CommRing→Ring R) n ∘∙ ≃∙map e
+
+  private
+    module hlevcon =
+      isConnectedPoint 2 conB
+        (λ a → isProp→isSet (
+          isPropIsOfHLevel {A = (Q a →∙ EMR∙ n)} 2))
+        (pt B , isOfHLevelRetractFromIso 2
+                 (post∘∙equiv e)
+                 (isSet-Sn→∙EM RR n))
+
+    module con =
+      isConnectedPoint 2 conB
+       hlevcon.elim ((pt B) , Q*→EM)
+
+  isSetQ→ : (b : fst B) → isSet (Q b →∙ EMR∙ n)
+  isSetQ→ = hlevcon.elim
+
+  c : (b : fst B) → Q b →∙ EMR∙ n
+  c = con.elim
+
+  c-id : c (pt B) ≡ Q*→EM
+  c-id = con.β
+
+  module preThom-inst =
+    preThom B Q (isConnectedSubtr 2 1 conB) R n e c c-id
+
+  g : (i : ℕ) (b : fst B) → EMR i → Q b →∙ EMR∙ (i +' n)
+  g = preThom-inst.g
+
+  isEquiv-g : (i : ℕ) (b : fst B) → isEquiv (g i b)
+  isEquiv-g i b = preThom-inst.g-equiv i b .snd
+
+  ϕ : (i : ℕ) → (fst B → EMR i) → (b : fst B) → Q b →∙ EMR∙ (i +' n)
+  ϕ = preThom-inst.pre-ϕ
+
+  isEquivϕ : (i : ℕ) → isEquiv (ϕ i)
+  isEquivϕ = preThom-inst.isEq-ϕ
+
+  ϕIso : (i : ℕ)
+    → Iso (fst B → EMR i) ((b : fst B) → Q b →∙ EMR∙ (i +' n))
+  ϕIso = preThom-inst.pre-ϕIso
+
+-- Now for the 'true' Thom isomphism:
+module Thom (B : Pointed ℓ)
+         (P : fst B → Type ℓ')
+         (P* : P (pt B))
+         (conB : isConnected 2 (fst B))
+         (R : CommRing ℓ'')
+         where
+  private
+    RR = (CommRing→AbGroup R)
+    EMR = EM RR
+    EMR∙ = EM∙ RR
+    * = snd B
+
+  E = Σ[ x ∈ fst B ] (P x)
+
+  E∙ : Pointed _
+  fst E∙ = E
+  snd E∙ = * , P*
+
+  πE : E → fst B
+  πE = fst
+
+  -- goal: relate cohomology of B to cohomology of
+  -- the cofibre of πE:
+  EP : Type _
+  EP = Pushout (λ _ → tt) πE
+
+  EP∙ : Pointed _
+  fst EP∙ = EP
+  snd EP∙ = inr (pt B)
+
+  EP-contr : isContr E → Iso EP (fst B)
+  Iso.fun (EP-contr c) (inl x) = pt B
+  Iso.fun (EP-contr c) (inr x) = x
+  Iso.fun (EP-contr c) (push a i) = πE (isContr→isProp c (* , P*) a i)
+  Iso.inv (EP-contr c) = inr
+  Iso.rightInv (EP-contr c) = λ _ → refl
+  Iso.leftInv (EP-contr c) (inl x) = sym (push (* , P*))
+  Iso.leftInv (EP-contr c) (inr x) = refl
+  Iso.leftInv (EP-contr c) (push a i) j =
+    hcomp (λ k → λ {(i = i0) → push (* , P*) (~ j)
+                   ; (i = i1) → push a (~ j ∨ k)
+                   ; (j = i0) → inr (πE (isContr→isProp c (* , P*) a i))
+                   ; (j = i1) → push a (i ∧ k)})
+      (push (isContr→isProp c (* , P*) a i) (~ j))
+
+  -- Main goal: establish ((b : fst B) → Q b →∙ EMR∙ k) ≃ (EP∙ →∙ EMR∙ k)
+  -- Combined with the previous isos, this gives the Thom isomorphism
+  -- Hⁱ(B,R) ≃ Hⁱ⁺ⁿ(EP∙,R)
+  Q : fst B → Pointed ℓ'
+  Q b = Susp (P b) , north
+
+  F = Σ[ x ∈ fst B ] (Q x .fst)
+
+  B→F : fst B → F
+  B→F b = b , north
+
+  FP : Type _
+  FP = Pushout (λ _ → tt) B→F
+
+  FP∙ : Pointed _
+  fst FP∙ = FP
+  snd FP∙ = inr (pt B , north)
+
+  -- step 1: show EP∙ ≃ FP∙, and thus (EP∙ →∙ EMR∙ k) ≃ (FP∙ →∙ EMR∙ k)
+  EP→FP : EP → FP
+  EP→FP (inl x) = inl x
+  EP→FP (inr x) = inr (x , south)
+  EP→FP (push (e , p) i) =
+    (push e ∙ λ j → inr (e , merid p j)) i
+
+  FP→EP : FP → EP
+  FP→EP (inl x) = inl x
+  FP→EP (inr (x , north)) = inl tt
+  FP→EP (inr (x , south)) = inr x
+  FP→EP (inr (x , merid a i)) = push (x , a) i
+  FP→EP (push a i) = inl tt
+
+  Iso-EP-FP : Iso EP FP
+  Iso.fun Iso-EP-FP = EP→FP
+  Iso.inv Iso-EP-FP = FP→EP
+  Iso.rightInv Iso-EP-FP (inl x) = refl
+  Iso.rightInv Iso-EP-FP (inr (x , north)) = push x
+  Iso.rightInv Iso-EP-FP (inr (x , south)) = refl
+  Iso.rightInv Iso-EP-FP (inr (x , merid a i)) j =
+    compPath-filler' (push x) (λ j₁ → inr (x , merid a j₁)) (~ j) i
+  Iso.rightInv Iso-EP-FP (push a i) j = push a (i ∧ j)
+  Iso.leftInv Iso-EP-FP (inl x) = refl
+  Iso.leftInv Iso-EP-FP (inr x) = refl
+  Iso.leftInv Iso-EP-FP (push (b , p) i) j =
+     (cong-∙ FP→EP (push b) (λ j → inr (b , merid p j))
+    ∙ sym (lUnit (push (b , p)))) j i
+
+  EP∙≃FP∙ : EP∙ ≃∙ FP∙
+  fst EP∙≃FP∙ = isoToEquiv Iso-EP-FP
+  snd EP∙≃FP∙ i = inr (pt B , merid P* (~ i))
+
+  -- step 2: show (FP∙ →∙ A) ≃ ((b : fst B) → Q b →∙ A) for any pointed type A
+  -- (taken homogeneous for convenience)
+  mapIso : ∀ {ℓ} {A : Pointed ℓ}
+    → (isHomogeneous A)
+    → Iso ((FP , inr ((pt B) , north)) →∙ A)
+           ((b : fst B) → Q b →∙ A)
+  fst (Iso.fun (mapIso isHom) r b) y = fst r (inr (b , y))
+  snd (Iso.fun (mapIso isHom) r b) =
+    cong (fst r) (sym (push b) ∙ push (snd B)) ∙ snd r
+  fst (Iso.inv (mapIso {A = A} isHom) r) (inl x) = pt A
+  fst (Iso.inv (mapIso isHom) r) (inr (b , p)) = r b .fst p
+  fst (Iso.inv (mapIso isHom) r) (push a i) = r a .snd (~ i)
+  snd (Iso.inv (mapIso isHom) r) = r (pt B) .snd
+  Iso.rightInv (mapIso isHom) r = funExt λ b → →∙Homogeneous≡ isHom refl
+  Iso.leftInv (mapIso isHom) r =
+    →∙Homogeneous≡ isHom
+      (funExt λ { (inl x) → sym (snd r) ∙ cong (fst r) (sym (push (pt B)))
+                ; (inr x) → refl
+                ; (push a i) j → h a i j})
+    where
+    h : (a : fst B)
+      → Square (sym (snd r) ∙ cong (fst r) (sym (push (pt B))))
+               refl
+               (sym (cong (fst r)
+                 (sym (push a) ∙ push (pt B)) ∙ snd r))
+               (cong (r .fst) (push a))
+    h a = flipSquare
+      ((symDistr (cong (fst r) (sym (push a) ∙ push (pt B)))
+                       (snd r)
+        ∙∙ cong (sym (snd r) ∙_)
+            (cong (cong (fst r)) (symDistr (sym (push a)) (push (pt B)))
+            ∙ cong-∙ (fst r) (sym (push (pt B))) (push a))
+        ∙∙ assoc (sym (snd r))
+                 (cong (fst r) (sym (push (pt B))))
+                 (cong (fst r) (push a)))
+      ◁ flipSquare
+         λ i j → compPath-filler' (sym (snd r)
+                         ∙ cong (fst r) (sym (push (pt B))))
+                         (cong (fst r) (push a)) (~ j) i)
+
+  -- We get our first iso
+  ι : (k : ℕ) → Iso ((b : fst B) → Q b →∙ EMR∙ k) (EP∙ →∙ EMR∙ k)
+  ι k =
+    compIso (invIso (mapIso (isHomogeneousEM _)))
+      (post∘∙equiv (invEquiv∙ EP∙≃FP∙))
+
+  -- we need it to be structure preserving in the obvious way
+  ι⁻-pres+ : (k : ℕ) (f g : EP∙ →∙ EMR∙ k)
+    → Iso.inv (ι k) (f +ₖ∙ g) ≡
+     λ b → (Iso.inv (ι k) f b) +ₖ∙ (Iso.inv (ι k) g b)
+  ι⁻-pres+ k f g = funExt λ b
+    → →∙Homogeneous≡
+      (isHomogeneousEM k)
+      (funExt λ { north → refl
+                ; south → refl
+                ; (merid a i) → refl})
+
+  ι-pres+ : (k : ℕ) (f g : (b : fst B) → Q b →∙ EMR∙ k)
+    → Iso.fun (ι k) (λ b → f b +ₖ∙ g b)
+     ≡ Iso.fun (ι k) f +ₖ∙ Iso.fun (ι k) g
+  ι-pres+ k = morphLemmas.isMorphInv _+ₖ∙_ (λ f g b → f b +ₖ∙ g b)
+              (Iso.inv (ι k)) (ι⁻-pres+ k)
+              (Iso.fun (ι k))
+              (Iso.leftInv (ι k)) (Iso.rightInv (ι k))
+
+  -- We combine it with the generalised thom iso, in order to get the
+  -- usual Thom isomorphism
+
+  module _  (n : ℕ) (e : (P (pt B) , P*) ≃∙ S₊∙ n) where
+    Q≃ : Q (pt B) ≃∙ S₊∙ (suc n)
+    Q≃ = compEquiv∙
+          (isoToEquiv
+           (congSuspIso
+            (equivToIso (fst e))) , refl)
+            (isoToEquiv (invIso (IsoSucSphereSusp n))
+              , IsoSucSphereSusp∙ n)
+
+    module con (c : (b : fst B) → Q b →∙ EM∙ (CommRing→AbGroup R) (suc n))
+           (r : c (pt B) ≡ (gen-HⁿSⁿ-raw (CommRing→Ring R) (suc n) ∘∙ ≃∙map Q≃))
+           where
+      module M = preThom B Q conB R (suc n) Q≃ c r
+
+      -- Finally, the actual Thom ismorphism
+      ϕ-raw : (i : ℕ) → (fst B → EMR i) ≃ (EP∙ →∙ EMR∙ (i +' suc n))
+      ϕ-raw i = isoToEquiv (compIso (M.pre-ϕIso i) (ι (i +' (suc n))))
+
+      ϕ-equiv : (i : ℕ) → coHom i RR (fst B) ≃ coHomRed (i +' suc n) RR EP∙
+      ϕ-equiv i =
+        isoToEquiv (setTruncIso (compIso (M.pre-ϕIso i) (ι (i +' (suc n)))))
+
+      ϕ-raw-contr : (i : ℕ) → isContr E → (fst B → EMR i) ≃ (B →∙ EMR∙ (i +' suc n))
+      ϕ-raw-contr i contr =
+        compEquiv (ϕ-raw i)
+          (isoToEquiv (post∘∙equiv (isoToEquiv (EP-contr contr) , refl)))
+
+      ϕ : (i : ℕ) → coHom i RR (fst B) → coHomRed (i +' suc n) RR EP∙
+      ϕ i = ϕ-equiv i .fst
+
+      isHomϕ : (i : ℕ)
+        → (x y : coHom i RR (fst B)) → ϕ i (x +ₕ y) ≡ ϕ i x +ₕ∙ ϕ i y
+      isHomϕ i =
+        ST.elim2 (λ _ _ → isSetPathImplicit)
+          λ f g → cong ∣_∣₂ (cong (Iso.fun (ι (i +' suc n)))
+                             (M.pre-ϕ-pres+ i f g)
+                          ∙ ι-pres+ (i +' suc n)
+                             (λ b → M.g i b (f b)) (λ b → M.g i b (g b))
+                          ∙ →∙Homogeneous≡ (isHomogeneousEM (i +' suc n)) refl)
+
+      ϕHom : (i : ℕ) → AbGroupHom (coHomGr i RR (fst B))
+                                    (coHomRedGr (i +' suc n) RR EP∙)
+      fst (ϕHom i) = ϕ i
+      snd (ϕHom i) = makeIsGroupHom (isHomϕ i)
+
+      ϕGrEquiv : (i : ℕ) → AbGroupEquiv (coHomGr i RR (fst B))
+                                          (coHomRedGr (i +' suc n) RR EP∙)
+      fst (ϕGrEquiv i) = ϕ-equiv i
+      snd (ϕGrEquiv i) = ϕHom i .snd
+
+  -- For the Gysin sequence, we will be need the long exact sequence
+  -- in cohomology related to the cofibre EP∙, i.e.
+  -- ... → Hⁱ⁻¹(E,R) → H̃ⁱ(EP∙,R) → Hⁱ(B,R) → Hⁱ(E,R) → ...
+  pre-E↑ : (i : ℕ) → (E → EM RR i) → EP∙ →∙ EM∙ RR (suc i)
+  fst (pre-E↑ i f) (inl x) = 0ₖ (suc i)
+  fst (pre-E↑ i f) (inr x) = 0ₖ (suc i)
+  fst (pre-E↑ i f) (push a i₁) = EM→ΩEM+1 i (f a) i₁
+  snd (pre-E↑ i f) = refl
+
+  E↑ : (i : ℕ) → AbGroupHom (coHomGr i RR E) (coHomRedGr (suc i) RR EP∙)
+  fst (E↑ i) = ST.map (pre-E↑ i)
+  snd (E↑ i) =
+    makeIsGroupHom
+      (ST.elim2 (λ _ _ → isSetPathImplicit)
+        λ f g → cong ∣_∣₂
+          (→∙Homogeneous≡ (isHomogeneousEM (suc i))
+           (funExt λ { (inl x) → sym (rUnitₖ (suc i) (0ₖ (suc i)))
+                     ; (inr x) → sym (rUnitₖ (suc i) (0ₖ (suc i)))
+                     ; (push a j) → flipSquare (help i (f a) (g a)) j})))
+    where
+    help : (i : ℕ) (x y : EM RR i)
+      → PathP (λ j → rUnitₖ {G = RR} (suc i) (0ₖ (suc i)) (~ j)
+                   ≡ rUnitₖ (suc i) (0ₖ (suc i)) (~ j))
+               (EM→ΩEM+1 {G = RR} i (x +ₖ y))
+               (cong₂ _+ₖ_ (EM→ΩEM+1 i x) (EM→ΩEM+1 i y))
+    help zero x y = EM→ΩEM+1-hom zero x y
+                  ∙ sym (cong₂+₁ (EM→ΩEM+1 zero x) (EM→ΩEM+1 zero y))
+    help (suc n) x y = EM→ΩEM+1-hom (suc n) x y
+                  ∙ sym (cong₂+₂ n (EM→ΩEM+1 (suc n) x)
+                                 (EM→ΩEM+1 (suc n) y))
+
+  j* : (i : ℕ) → AbGroupHom (coHomRedGr i RR EP∙) (coHomGr i RR (fst B))
+  fst (j* i) = ST.map λ f b → fst f (inr b)
+  snd (j* i) = makeIsGroupHom
+    (ST.elim2 (λ _ _ → isSetPathImplicit) λ f g → refl)
+
+  p* : (i : ℕ) → AbGroupHom (coHomGr i RR (fst B)) (coHomGr i RR E)
+  p* i = coHomHom i fst
+
+  Im-j*⊂Ker-p* : (i : ℕ) (x : _)
+    → isInIm (j* i) x
+    → isInKer (p* i) x
+  Im-j*⊂Ker-p* i =
+    ST.elim
+      (λ f → isSetΠ λ _ → isSetPathImplicit)
+      λ f → PT.rec (squash₂ _ _)
+        (uncurry (ST.elim (λ _ → isSetΠ
+          λ _ → isSetPathImplicit)
+          λ g p → PT.rec (squash₂ _ _)
+            (J (λ f _ → isInKer (p* i) ∣ f ∣₂)
+              (cong ∣_∣₂ (funExt (λ a
+              → cong (fst g) (sym (push a) ∙ push (pt B , P*))
+              ∙ snd g))))
+            (Iso.fun PathIdTrunc₀Iso p)))
+
+  Ker-p*⊂Im-j* : (i : ℕ) (x : _)
+    → isInKer (p* i) x
+    → isInIm (j* i) x
+  Ker-p*⊂Im-j* i =
+    ST.elim (λ _ → isSetΠ λ _ → isProp→isSet squash₁)
+     λ f p → PT.map
+       (λ p → ∣ (λ { (inl x) → 0ₖ i
+                   ; (inr x) → f x
+                   ; (push a i) → p (~ i) a})
+             , funExt⁻ p (pt B , P*) ∣₂
+             , refl)
+       (Iso.fun PathIdTrunc₀Iso p)
+
+  Im-p*⊂Ker-E↑ : (i : ℕ) (x : _)
+    → isInIm (p* i) x
+    → isInKer (E↑ i) x
+  Im-p*⊂Ker-E↑ i = ST.elim
+      (λ f → isSetΠ λ _ → isSetPathImplicit)
+      λ f → PT.rec (squash₂ _ _)
+         (uncurry (ST.elim (λ _ → isSetΠ
+          λ _ → isSetPathImplicit)
+          λ g p → PT.rec (squash₂ _ _)
+            (J (λ f _ → isInKer (E↑ i) ∣ f ∣₂)
+              (cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM _)
+                (funExt λ { (inl x) → refl
+                          ; (inr x) → sym (EM→ΩEM+1 i (g x))
+                          ; (push a j) k
+                            → EM→ΩEM+1 i (g (fst a)) (j ∧ ~ k)}))))
+            (Iso.fun PathIdTrunc₀Iso p)))
+
+  Ker-E↑⊂Im-p* : (i : ℕ) (x : _)
+    → isInKer (E↑ i) x
+    → isInIm (p* i) x
+  Ker-E↑⊂Im-p* i =
+    ST.elim (λ _ → isSetΠ λ _ → isProp→isSet squash₁)
+      λ f p → PT.map (λ r →
+        ∣ (λ b → ΩEM+1→EM i (sym (funExt⁻ (cong fst r) (inr b)))
+                             +ₖ f (* , P*)) ∣₂
+      , cong ∣_∣₂ (funExt λ {(x , p)
+        → cong (_+ₖ f (* , P*))
+             ((cong (ΩEM+1→EM i)
+            (cong sym (sym (fromPathP (cong (funExt⁻ (cong fst r)) (push (x , p))))
+                    ∙ (λ j → transp (λ k → EM→ΩEM+1 i (f (x , p)) (j ∨ k)
+                                           ≡ 0ₖ (suc i))
+                         j (compPath-filler'
+                            (sym (EM→ΩEM+1 i (f (x , p))))
+                            (funExt⁻ (cong fst r) (inl tt)) j)))
+            ∙ (symDistr (sym (EM→ΩEM+1 i (f (x , p))))
+                        (funExt⁻ (λ i₂ → fst (r i₂)) (inl tt))))
+          ∙ ΩEM+1→EM-hom i
+              (sym (funExt⁻ (λ i₁ → fst (r i₁)) (inl tt)))
+              (EM→ΩEM+1 i (f (x , p))))
+            ∙ cong₂ _+ₖ_
+               (cong (ΩEM+1→EM i)
+                 (cong sym
+                   (rUnit _ ∙∙ sym (Square→compPath
+                   ((cong (funExt⁻ (cong fst r)) (push (* , P*)))
+                 ▷ λ i j → r j .snd i)) ∙∙ sym (rUnit _))))
+               (Iso.leftInv (Iso-EM-ΩEM+1 i) (f (x , p))))
+         ∙ cong₂ _+ₖ_ (cong₂ _+ₖ_ (cong (ΩEM+1→EM i)
+                       (sym (EM→ΩEM+1-sym i (f (* , P*))))
+                      ∙ Iso.leftInv (Iso-EM-ΩEM+1 i) (-ₖ (f (* , P*)))) refl
+                    ∙ commₖ i (-ₖ f (* , P*)) (f (x , p)))
+                    refl
+         ∙ sym (assocₖ i (f (x , p)) (-ₖ (f (* , P*))) (f (* , P*)))
+         ∙ cong₂ _+ₖ_ refl (lCancelₖ i (f (* , P*)))
+         ∙ rUnitₖ i (f (x , p))}))
+        ((Iso.fun PathIdTrunc₀Iso p))
+
+  Im-E↑⊂Ker-j* : (i : ℕ) (x : _)
+    → isInIm (E↑ i) x
+    → isInKer (j* (suc i)) x
+  Im-E↑⊂Ker-j* i = ST.elim
+      (λ f → isSetΠ λ _ → isSetPathImplicit)
+      λ f → PT.rec (squash₂ _ _)
+         (uncurry (ST.elim (λ _ → isSetΠ
+          λ _ → isSetPathImplicit)
+          λ g p → PT.rec (squash₂ _ _)
+            (J (λ f _ → isInKer (j* (suc i)) ∣ f ∣₂) refl)
+            (Iso.fun PathIdTrunc₀Iso p)))
+
+  Ker-j*⊂Im-E↑ : (i : ℕ) (x : _)
+    → isInKer (j* (suc i)) x
+    → isInIm (E↑ i) x
+  Ker-j*⊂Im-E↑ i =
+    ST.elim (λ _ → isSetΠ λ _ → isProp→isSet squash₁)
+      λ f p → PT.map
+       (λ p → ∣ (λ b → ΩEM+1→EM i (pth b f (funExt⁻ p))) ∣₂
+            , cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM _)
+              (funExt λ { (inl x) → sym (snd f)
+                                   ∙ cong (fst f) (sym (push (* , P*)))
+                        ; (inr x) → sym (funExt⁻ p x)
+                        ; (push a j) → main a f (funExt⁻ p) j})))
+       (Iso.fun PathIdTrunc₀Iso p)
+    where
+    pth : (a : E) (f : EP∙ →∙ EM∙ RR (suc i))
+       (p : (b : fst B) → fst f (inr b) ≡ 0ₖ (suc i))
+     → fst (Ω (EMR∙ (suc i)))
+    pth a f p = sym (snd f) ∙ cong (fst f) (sym (push (* , P*)))
+             ∙∙ cong (fst f) (push a)
+             ∙∙ p (fst a)
+
+    main : (a : E) (f : EP∙ →∙ EM∙ RR (suc i))
+       (p : (b : fst B) → fst f (inr b) ≡ 0ₖ (suc i))
+       →  PathP (λ j → EM→ΩEM+1 i (ΩEM+1→EM i (pth a f p)) j
+                 ≡ f .fst (push a j))
+            (sym (snd f) ∙ cong (fst f) (sym (push (* , P*))))
+            (sym (p (fst a)))
+    main a f p =
+      flipSquare (Iso.rightInv (Iso-EM-ΩEM+1 i) (pth a f p)
+               ◁ λ j i → doubleCompPath-filler
+                    (sym (snd f) ∙ cong (fst f) (sym (push (* , P*))))
+                    (cong (fst f) (push a))
+                    (p (fst a)) (~ j) i)
+
+module Gysin (B : Pointed ℓ)
+         (P : fst B → Type ℓ')
+         (conB : isConnected 2 (fst B))
+         (R : CommRing ℓ'')
+         (n : ℕ)
+         (eq' : P (pt B) ≃ S₊ n)
+         (c : (b : fst B) → Susp∙ (P b) →∙ EM∙ (CommRing→AbGroup R) (suc n))
+         (c-id : c (pt B) ≡ gen-HⁿSⁿ-raw
+           (CommRing→Ring R) (suc n)
+           ∘∙ ≃∙map (Thom.Q≃ B P (invEq eq' (ptSn n))
+              conB R n (eq' , (secEq eq' (ptSn n)))))
+         where
+  private
+     RR = (CommRing→AbGroup R)
+     EMR = EM RR
+     EMR∙ = EM∙ RR
+     P* = invEq eq' (ptSn n)
+  module M = Thom B P P* conB R
+  open M public
+
+  eq : (P (pt B) , P*) ≃∙ S₊∙ n
+  fst eq = eq'
+  snd eq = secEq eq' (ptSn n)
+
+  module _ (c-id : c (pt B) ≡ gen-HⁿSⁿ-raw (CommRing→Ring R) (suc n) ∘∙ ≃∙map (Q≃ n eq)) where
+    module L = con n eq c c-id
+    open L
+
+    -- The Euler class
+    e : coHom (suc n) RR (fst B)
+    e = ∣ (λ b → c b .fst south) ∣₂
+
+    minusPath : (i : ℕ) → (suc n ≤ i) → (i ∸ suc n) +' suc n ≡ i
+    minusPath i p = +'≡+ (i ∸ suc n) (suc n) ∙ ≤-∸-+-cancel p
+
+    -- The main map in the sequence
+    ⌣-hom : (i : ℕ) → (suc n ≤ i)
+      → AbGroupHom (coHomGr (i ∸ suc n) RR (fst B))
+                    (coHomGr i RR (fst B))
+    fst (⌣-hom i t) f =
+      subst (λ i → coHom i RR (fst B)) (minusPath i t) (f ⌣ e)
+    snd (⌣-hom i t) =
+      makeIsGroupHom
+          (λ f g → cong (subst (λ i₁ → coHom i₁ RR (fst B)) (minusPath i t))
+                      (distrR⌣ (i ∸ suc n) (suc n) f g e)
+                  ∙ IsGroupHom.pres· (snd (substℕ-coHom (minusPath i t)))
+                      (f ⌣ e) (g ⌣ e))
+
+    private
+      helpIso : (i : ℕ) → suc n ≤ i
+        → AbGroupEquiv (coHomRedGr i RR EP∙)
+            (coHomGr (i ∸ suc n) RR (fst B))
+      helpIso i t =
+        compGroupEquiv (substℕ-coHomRed (sym (minusPath i t)))
+            (invGroupEquiv (ϕGrEquiv (i ∸ suc n)))
+
+      alt-hom : (i : ℕ) → (suc n ≤ i)
+        → AbGroupHom (coHomGr (i ∸ suc n) RR (fst B))
+                      (coHomGr i RR (fst B))
+      alt-hom i t =
+        compGroupHom (ϕHom (i ∸ suc n))
+          (compGroupHom (j* _)
+          (GroupEquiv→GroupHom (substℕ-coHom (minusPath i t))))
+
+      ⌣≡alt : (i : ℕ) (t : suc n ≤ i)
+        → ⌣-hom i t ≡ alt-hom i t
+      ⌣≡alt i t = Σ≡Prop (λ _ → isPropIsGroupHom _ _)
+        (funExt (ST.elim (λ _ → isSetPathImplicit) λ _ → refl))
+
+
+    -- the other two maps
+    mapₗ : (i : ℕ) → suc n ≤ suc i
+        → AbGroupHom (coHomGr i RR E)
+                      (coHomGr (suc i ∸ suc n) RR (fst B))
+    mapₗ i t =
+      compGroupHom (E↑ i)
+         (GroupEquiv→GroupHom
+           (helpIso (suc i) t))
+
+    mapᵣ : (i : ℕ)
+        → AbGroupHom (coHomGr i RR (fst B))
+                      (coHomGr i RR E)
+    mapᵣ i = p* i
+
+
+    -- Finally: exactness
+    Im-mapᵣ⊂Ker-mapₗ : (i : ℕ) (t : suc n ≤ suc i) (x : coHom i RR E)
+      → isInIm (mapᵣ i) x
+      → isInKer (mapₗ i t) x
+    Im-mapᵣ⊂Ker-mapₗ i t x s =
+        cong (invEq (fst (ϕGrEquiv (suc i ∸ suc n))))
+          (cong (subst (λ i → coHomRed i RR EP∙) (sym (minusPath (suc i) t)))
+            (M.Im-p*⊂Ker-E↑ i x s))
+      ∙ IsGroupHom.pres1 (helpIso (suc i) t .snd)
+
+    Ker-mapₗ⊂Im-mapᵣ : (i : ℕ) (t : suc n ≤ suc i) (x : coHom i RR E)
+      → isInKer (mapₗ i t) x
+      → isInIm (mapᵣ i) x
+    Ker-mapₗ⊂Im-mapᵣ i t x p =
+      Ker-E↑⊂Im-p* i x
+        (sym (retEq (fst (helpIso (suc i) t)) (E↑ i .fst x))
+        ∙ cong (invEq (fst (helpIso (suc i) t))) p
+        ∙ IsGroupHom.pres1 (invGroupEquiv (helpIso (suc i) t) .snd))
+
+    private
+      j*≡ : (i : ℕ) (t : suc n ≤  i)
+         → (x : _) → j* i .fst x
+                     ≡ fst (alt-hom i t)
+                        (fst (helpIso i t) .fst x)
+      j*≡ i t f = cong (j* i .fst)
+               (sym (substSubst⁻ (λ i → coHomRed i RR EP∙) (minusPath i t) f))
+            ∙  sym (substCommSlice (λ i → coHomRed i RR EP∙)
+                 (λ i → coHom i RR (fst B)) (λ i → j* i .fst) (minusPath i t)
+                 (subst (λ i → coHomRed i RR EP∙) (sym (minusPath i t)) f))
+            ∙ cong (subst (λ i → coHom i RR (fst B)) (minusPath i t))
+                (cong (j* ((i ∸ suc n) +' (suc n)) .fst)
+                  (sym (secEq (ϕGrEquiv (i ∸ suc n) .fst)
+                    (subst (λ i → coHomRed i RR EP∙) (sym (minusPath i t))
+                      f))))
+
+    Ker-⌣⊂Im-mapₗ : (i : ℕ) (t : suc n ≤  suc i)
+      (x : coHom (suc i ∸ suc n) RR (fst B))
+      → isInKer (⌣-hom (suc i) t) x
+      → isInIm (mapₗ i t) x
+    Ker-⌣⊂Im-mapₗ i t x s =
+      →Im (Ker-j*⊂Im-E↑ i _
+          ((j*≡ (suc i) t _
+          ∙ cong (fst (alt-hom (suc i) t))
+            (secEq (fst (helpIso (suc i) t)) x))
+        ∙ funExt⁻ (cong fst (sym (⌣≡alt (suc i) t))) x ∙ s))
+      where
+      →Im : isInIm (E↑ i) (invEq (fst (helpIso (suc i) t)) x)
+        → isInIm (mapₗ i t) x
+      →Im = PT.map (uncurry λ f p → f
+                   , cong (fst (fst (helpIso (suc i) t))) p
+                   ∙ secEq (fst (helpIso (suc i) t)) _)
+
+
+    Im-mapₗ⊂Ker-⌣ : (i : ℕ) (t : suc n ≤  suc i)
+        (x : coHom (suc i ∸ suc n) RR (fst B))
+        → isInIm (mapₗ i t) x
+        → isInKer (⌣-hom (suc i) t) x
+    Im-mapₗ⊂Ker-⌣ i t x p =
+        (((λ j → ⌣≡alt (suc i) t j .fst x)
+      ∙ cong (fst (alt-hom (suc i) t))
+         (sym (secEq (fst (helpIso (suc i) t)) x)))
+      ∙ sym (j*≡ (suc i) t (invEq (helpIso (suc i) t .fst) x)))
+      ∙ Im-E↑⊂Ker-j* i _ (Im-transf x p)
+      where
+      Im-transf : (x : _) → isInIm (mapₗ i t) x
+        → isInIm (E↑ i) (invEq (helpIso (suc i) t .fst) x)
+      Im-transf f = PT.map (uncurry λ g p → g
+        , sym (retEq (helpIso (suc i) t .fst) (E↑ i .fst g))
+        ∙ cong (invEq (helpIso (suc i) t .fst)) p)
+
+    Im--⌣⊂Ker-mapᵣ : (i : ℕ) (t : suc n ≤ i) (x : coHom i RR (fst B))
+      → isInIm (⌣-hom i t) x
+      → isInKer (mapᵣ i) x
+    Im--⌣⊂Ker-mapᵣ i t x p =
+      Im-j*⊂Ker-p* i x
+        (PT.map
+          (uncurry (λ f p → invEq (helpIso i t .fst) f
+          , ((j*≡ i t (invEq (helpIso i t .fst) f)
+          ∙ cong (alt-hom i t .fst)
+             (secEq (fst (helpIso i t)) f))
+          ∙ ((λ j → ⌣≡alt i t (~ j) .fst f)))
+           ∙ refl
+          ∙ p)) p)
+
+
+    Ker-mapᵣ⊂Im--⌣ : (i : ℕ) (t : suc n ≤ i) (x : coHom i RR (fst B))
+      → isInKer (mapᵣ i) x
+      → isInIm (⌣-hom i t) x
+    Ker-mapᵣ⊂Im--⌣ i t x p =
+      subst (λ f → isInIm f x) (sym (⌣≡alt i t))
+        (→Im x (Ker-p*⊂Im-j* i x p))
+      where
+      →Im : (x : _) → isInIm (j* i) x → isInIm (alt-hom i t) x
+      →Im x = PT.map (uncurry λ f p → (fst (helpIso i t .fst) f)
+        , sym (j*≡ i t f)
+         ∙ p)
+
+
+
+module GysinCon (B : Pointed ℓ)
+         (P : fst B → Type ℓ')
+         (conB : isConnected 3 (fst B))
+         (R : CommRing ℓ'')
+         (n : ℕ)
+         (eq : P (pt B) ≃ S₊ n)
+         where
+  private
+    module T = Thom B P (invEq eq (ptSn n)) (isConnectedSubtr 2 1 conB) R
+    module GT = genThom B
+      (λ b → Susp∙ (P b)) conB R (suc n) (T.Q≃ n (eq , secEq eq (ptSn n)))
+
+  module Inst = Gysin B P (isConnectedSubtr 2 1 conB)
+                      R
+                      n
+                      eq
+                      GT.c
+                      GT.c-id
+
+  open Inst public
diff --git a/Cubical/Foundations/Pointed/Properties.agda b/Cubical/Foundations/Pointed/Properties.agda
index 9244485d90..13c36276ff 100644
--- a/Cubical/Foundations/Pointed/Properties.agda
+++ b/Cubical/Foundations/Pointed/Properties.agda
@@ -7,7 +7,9 @@ open import Cubical.Foundations.Function
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.HalfAdjoint
 open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Path
 
 open import Cubical.Data.Sigma
 
@@ -100,73 +102,106 @@ module _ {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B
   isInKer∙ : (x : fst A) → Type ℓ'
   isInKer∙ x = fst f x ≡ snd B
 
-pre∘∙equiv : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B C : Pointed ℓ'}
+private module _ {ℓA ℓB ℓC : Level} (A : Pointed ℓA) (B : Pointed ℓB) (C : Pointed ℓC) (e : A ≃∙ B) where
+  toEq : (A →∙ C) → (B →∙ C)
+  toEq = _∘∙ ≃∙map (invEquiv∙ e)
+
+  fromEq : B →∙ C → (A →∙ C)
+  fromEq = _∘∙ ≃∙map e
+
+  toEq' : (C →∙ A) → C →∙ B
+  toEq' = ≃∙map e ∘∙_
+
+  fromEq' : C →∙ B → (C →∙ A)
+  fromEq' = ≃∙map (invEquiv∙ e) ∘∙_
+
+pre∘∙equiv : ∀ {ℓA ℓB ℓC} {A : Pointed ℓA} {B : Pointed ℓB} {C : Pointed ℓC}
  → (B ≃∙ C) → Iso (A →∙ B) (A →∙ C)
-pre∘∙equiv {A = A} {B = B} {C = C} eq = main
+Iso.fun (pre∘∙equiv {A = A} {B = B} {C = C} e) = toEq' B C A e
+Iso.inv (pre∘∙equiv {A = A} {B = B} {C = C} e) = fromEq' B C A e
+Iso.rightInv (pre∘∙equiv {A = A} {B = B} {C = C} e) =
+  J (λ ptC p → section (toEq' B (fst C , ptC) A (fst e , p))
+                         (fromEq' B (fst C , ptC) A (fst e , p)))
+     (uncurry (λ f p → ΣPathP (funExt (λ x → isHAEquiv.rinv (HAe .snd) (f x))
+       , ((sym (rUnit _)
+        ∙ cong (cong (fst (fst e)))
+           λ i → cong (invEq (fst e)) p
+           ∙ (lUnit (retEq (fst e) (pt B)) (~ i)))
+           ∙ cong-∙ (fst (fst e))
+              (cong (invEq (fst e)) p)
+              (retEq (fst e) (pt B))
+           ∙ refl
+         ◁ flipSquare (((λ _ → isHAEquiv.rinv (HAe .snd) (f (pt A)))
+                      ∙ refl)
+                      ◁ lem _ _ _ _ (cong (isHAEquiv.rinv (HAe .snd)) p
+                                  ▷ sym (isHAEquiv.com (HAe .snd) (pt B))))))))
+     (snd e)
   where
-  module _ {ℓ ℓ' : Level} (A : Pointed ℓ) (B C : Pointed ℓ')
-           (eq : (B ≃∙ C)) where
-    to : (A →∙ B) → (A →∙ C)
-    to = ≃∙map eq ∘∙_
-
-    from : (A →∙ C) → (A →∙ B)
-    from = ≃∙map (invEquiv∙ eq) ∘∙_
-
-  lem : {ℓ  : Level} {B : Pointed ℓ}
-    → ≃∙map (invEquiv∙ {A = B} ((idEquiv (fst B)) , refl)) ≡ id∙ B
-  lem = ΣPathP (refl , (sym (lUnit _)))
-
-  J-lem : {ℓ ℓ' : Level} {A : Pointed ℓ} {B C : Pointed ℓ'}
-             → (eq : (B ≃∙ C))
-             → retract (to A B C eq) (from _ _ _ eq)
-              × section (to A B C eq) (from _ _ _ eq)
-  J-lem {A = A} {B = B} {C = C} =
-    Equiv∙J (λ B eq → retract (to A B C eq) (from _ _ _ eq)
-              × section (to A B C eq) (from _ _ _ eq))
-            ((λ f → ((λ i → (lem i ∘∙ (id∙ C ∘∙ f)))
-                  ∙ λ i → ∘∙-idʳ (∘∙-idʳ f i) i))
-            , λ f → ((λ i → (id∙ C ∘∙ (lem i ∘∙ f)))
-                  ∙ λ i → ∘∙-idʳ (∘∙-idʳ f i) i))
-
-  main : Iso (A →∙ B) (A →∙ C)
-  Iso.fun main = to A B C eq
-  Iso.inv main = from A B C eq
-  Iso.rightInv main = J-lem eq .snd
-  Iso.leftInv main = J-lem eq .fst
-
-post∘∙equiv : ∀ {ℓ ℓC} {A B : Pointed ℓ} {C : Pointed ℓC}
+  HAe = equiv→HAEquiv (fst e)
+  lem : ∀ {ℓ} {A : Type ℓ} {x y z w : A}
+      (p : x ≡ y) (q : y ≡ z) (r : x ≡ w) (l : w ≡ z)
+    → PathP (λ i → p i ≡ l i) r q
+    → PathP (λ i → (p ∙ q) i ≡ l i) r refl
+  lem p q r l P i j =
+    hcomp (λ k → λ{ (i = i0) → r j
+                   ; (i = i1) → q (j ∨ k)
+                   ; (j = i1) → l i})
+          (P i j)
+Iso.leftInv (pre∘∙equiv {A = A} {B = B} {C = C} e) =
+  J (λ pt p → retract (toEq' B (fst C , pt) A (fst e , p))
+                       (fromEq' B (fst C , pt) A (fst e , p)))
+    (uncurry (λ f →
+      J (λ ptB p
+       → fromEq' (fst B , ptB)
+                  (fst C , fst (fst e) ptB) A (fst e , refl)
+           (toEq' (fst B , ptB)
+                  (fst C , fst (fst e) ptB) A (fst e , refl) (f , p))
+         ≡ (f , p))
+         (ΣPathP
+          (funExt (λ x → retEq (fst e) (f x))
+         , ((cong₂ _∙_ ((λ i → cong (invEq (fst e)) (lUnit refl (~ i))))
+                       (sym (lUnit _) ∙ λ _ → retEq (fst e) (f (pt A)))
+          ∙ sym (lUnit _))
+         ◁ λ i j → retEq (fst e) (f (pt A)) (i ∨ j))))))
+    (snd e)
+
+post∘∙equiv : ∀ {ℓA ℓB ℓC} {A : Pointed ℓA} {B : Pointed ℓB} {C : Pointed ℓC}
   → (A ≃∙ B) → Iso (A →∙ C) (B →∙ C)
-post∘∙equiv {A = A} {B = B} {C = C} eq = main
+Iso.fun (post∘∙equiv {A = A} {B = B} {C = C} e) = toEq A B C e
+Iso.inv (post∘∙equiv {A = A} {B = B} {C = C} e) = fromEq A B C e
+Iso.rightInv (post∘∙equiv {A = A}{B = B , ptB} {C = C} e) =
+  J (λ pt p → section (toEq A (B , pt) C (fst e , p))
+                        (fromEq A (B , pt) C (fst e , p)))
+     (uncurry (λ f →
+       J (λ ptC p → toEq A (B , fst (fst e) (pt A)) (fst C , ptC) (fst e , refl)
+                      (fromEq A (B , fst (fst e) (pt A)) (fst C , ptC) (fst e , refl)
+                        (f , p))
+                   ≡ (f , p))
+         (ΣPathP (funExt (λ x → cong f (isHAEquiv.rinv (snd HAe) x))
+           , (cong₂ _∙_
+               (λ i → cong f (cong (fst (fst e)) (lUnit (retEq (fst e) (pt A)) (~ i))))
+               (sym (rUnit refl))
+           ∙ sym (rUnit _)
+           ∙ cong (cong f) (isHAEquiv.com (snd HAe) (pt A)))
+         ◁ λ i j → f (isHAEquiv.rinv (snd HAe) (fst HAe (pt A)) (i ∨ j))))))
+     (snd e)
   where
-  module _ {ℓ ℓC : Level} (A B : Pointed ℓ) (C : Pointed ℓC)
-           (eq : (A ≃∙ B)) where
-    to : (A →∙ C) → (B →∙ C)
-    to = _∘∙ ≃∙map (invEquiv∙ eq)
-
-    from : (B →∙ C) → (A →∙ C)
-    from = _∘∙ ≃∙map eq
-
-  lem : {ℓ  : Level} {B : Pointed ℓ}
-    → ≃∙map (invEquiv∙ {A = B} ((idEquiv (fst B)) , refl)) ≡ id∙ B
-  lem = ΣPathP (refl , (sym (lUnit _)))
-
-  J-lem : {ℓ ℓC : Level} {A B : Pointed ℓ} {C : Pointed ℓC}
-             → (eq : (A ≃∙ B))
-             → retract (to A B C eq) (from _ _ _ eq)
-              × section (to A B C eq) (from _ _ _ eq)
-  J-lem {B = B} {C = C} =
-    Equiv∙J (λ A eq → retract (to A B C eq) (from _ _ _ eq)
-              × section (to A B C eq) (from _ _ _ eq))
-            ((λ f → ((λ i → (f ∘∙ lem i) ∘∙ id∙ B)
-                  ∙ λ i → ∘∙-idˡ (∘∙-idˡ f i) i))
-           , λ f → (λ i → (f ∘∙ id∙ B) ∘∙ lem i)
-                  ∙ λ i → ∘∙-idˡ (∘∙-idˡ f i) i)
-
-  main : Iso (A →∙ C) (B →∙ C)
-  Iso.fun main = to A B C eq
-  Iso.inv main = from A B C eq
-  Iso.rightInv main = J-lem eq .snd
-  Iso.leftInv main = J-lem eq .fst
+  HAe = equiv→HAEquiv (fst e)
+Iso.leftInv (post∘∙equiv {A = A} {B = B , ptB} {C = C} e) =
+  J (λ pt p → retract (toEq A (B , pt) C (fst e , p))
+                        (fromEq A (B , pt) C (fst e , p)))
+     (uncurry (λ f → J (λ ptC y →
+       fromEq A (B , fst (fst e) (pt A)) (fst C , ptC) (fst e , refl)
+        (toEq A (B , fst (fst e) (pt A)) (fst C , ptC) (fst e , refl)
+        (f , y))
+      ≡ (f , y))
+      (ΣPathP (funExt (λ x → cong f (retEq (fst e) x))
+            , (sym (lUnit _)
+              ∙ sym (rUnit _)
+              ∙ cong (cong f) (sym (lUnit _))
+              ∙ (λ _ → cong f (retEq (fst e) (pt A)))
+             ◁ λ i j → f (retEq (fst e) (pt A) (i ∨ j)))))))
+     (snd e)
 
 flip→∙∙ : {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓA}
   → (A →∙ (B →∙ C ∙)) → B →∙ (A →∙ C ∙)
@@ -190,3 +225,12 @@ Iso.leftInv flip→∙∙Iso _ = refl
                 × (≃∙map f ∘∙ ≃∙map (invEquiv∙ f) ≡ idfun∙ B))
           ((ΣPathP (refl , sym (lUnit _) ∙ sym (rUnit refl)))
          , (ΣPathP (refl , sym (rUnit _) ∙ sym (rUnit refl))))
+
+pointedSecIso : ∀ {ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} (Q : fst A → Pointed ℓ'')
+  → Iso ((a : fst A) → Q a →∙ B)
+         (Σ[ F ∈ (Σ (fst A) (fst ∘ Q) → fst B) ]
+           ((a : fst A) → F (a , pt (Q a)) ≡ pt B))
+Iso.fun (pointedSecIso Q) F = (λ x → F (fst x) .fst (snd x)) , (λ x → F x .snd)
+Iso.inv (pointedSecIso Q) F a = (fst F ∘ (a ,_)) , snd F a
+Iso.rightInv (pointedSecIso Q) F = refl
+Iso.leftInv (pointedSecIso Q) F = refl
diff --git a/Cubical/Foundations/Transport.agda b/Cubical/Foundations/Transport.agda
index d4b9e156e4..72b084f241 100644
--- a/Cubical/Foundations/Transport.agda
+++ b/Cubical/Foundations/Transport.agda
@@ -96,6 +96,13 @@ Iso.inv (pathToIso x) = transport⁻ x
 Iso.rightInv (pathToIso x) = transportTransport⁻ x
 Iso.leftInv (pathToIso x) = transport⁻Transport x
 
+substIso : ∀ {ℓ ℓ'} {A : Type ℓ} (B : A → Type ℓ') {x y : A} (p : x ≡ y) → Iso (B x) (B y)
+substIso B p = pathToIso (cong B p)
+
+-- Redefining substEquiv in terms of substIso gives an explicit inverse
+substEquiv' : ∀ {ℓ ℓ'} {A : Type ℓ} (B : A → Type ℓ') {x y : A} (p : x ≡ y) → B x ≃ B y
+substEquiv' B p = isoToEquiv (substIso B p)
+
 isInjectiveTransport : ∀ {ℓ : Level} {A B : Type ℓ} {p q : A ≡ B}
   → transport p ≡ transport q → p ≡ q
 isInjectiveTransport {p = p} {q} α i =
diff --git a/Cubical/HITs/Susp/Properties.agda b/Cubical/HITs/Susp/Properties.agda
index f510599c11..4a9358a86d 100644
--- a/Cubical/HITs/Susp/Properties.agda
+++ b/Cubical/HITs/Susp/Properties.agda
@@ -55,7 +55,7 @@ Susp≃joinBool = isoToEquiv Susp-iso-joinBool
 Susp≡joinBool : ∀ {ℓ} {A : Type ℓ} → Susp A ≡ join A Bool
 Susp≡joinBool = isoToPath Susp-iso-joinBool
 
-congSuspIso : ∀ {ℓ} {A B : Type ℓ} → Iso A B → Iso (Susp A) (Susp B)
+congSuspIso : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → Iso A B → Iso (Susp A) (Susp B)
 fun (congSuspIso is) = suspFun (fun is)
 inv (congSuspIso is) = suspFun (inv is)
 rightInv (congSuspIso is) north = refl
diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda
index 1289e5f00b..d865dfe0dc 100644
--- a/Cubical/Homotopy/Connected.agda
+++ b/Cubical/Homotopy/Connected.agda
@@ -17,18 +17,19 @@ open import Cubical.Functions.Fibration
 open import Cubical.Functions.FunExtEquiv
 
 open import Cubical.Data.Unit
-open import Cubical.Data.Bool
-open import Cubical.Data.Nat
+open import Cubical.Data.Bool hiding (elim)
+open import Cubical.Data.Nat hiding (elim)
 open import Cubical.Data.Sigma
 
-open import Cubical.HITs.Nullification
+open import Cubical.HITs.Nullification hiding (elim)
 open import Cubical.HITs.Susp
 open import Cubical.HITs.SmashProduct
 open import Cubical.HITs.Pushout
 open import Cubical.HITs.Join
 open import Cubical.HITs.Sn.Base
-open import Cubical.HITs.S1
-open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec)
+open import Cubical.HITs.S1 hiding (elim)
+open import Cubical.HITs.Truncation as Trunc
+  renaming (rec to trRec) hiding (elim)
 
 open import Cubical.Homotopy.Loopspace
 
@@ -109,6 +110,16 @@ module elim {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} (f : A → B) wher
             (λ {(a , p) i → transp (λ j → P (p (j ∨ i)) .fst) i (s (p i))})
             (fConn b .fst)
 
+  isIsoPrecomposeβ : ∀ {ℓ'''} (n : ℕ) (P : B → TypeOfHLevel ℓ''' n)
+                   → (e : isConnectedFun n f)
+                   → (g : ((a : A) → P (f a) .fst))
+                   → (a : A)
+                   → Iso.inv (isIsoPrecompose n P e) g (f a) ≡ g a
+  isIsoPrecomposeβ zero P e g a = P (f a) .snd .snd (g a)
+  isIsoPrecomposeβ (suc n) P e g a =
+      cong (inv n P g (f a)) (e (f a) .snd ∣ a , refl ∣)
+    ∙ transportRefl _
+
   isEquivPrecompose : ∀ {ℓ'''} (n : ℕ) (P : B → TypeOfHLevel ℓ''' n)
                    → isConnectedFun n f
                    → isEquiv (λ(s : (b : B) → P b .fst) → s ∘ f)
@@ -402,6 +413,23 @@ isConnectedPoint2 n {A = A} a connMap = indMapEquiv→conType _ λ B → isoToIs
     Iso.rightInv theIso f = funExt λ y → sym (helper f y)
     Iso.leftInv theIso _ = refl
 
+module isConnectedPoint {ℓ ℓ'} (n : HLevel) {A : Type ℓ}
+     {B : A → Type ℓ'}
+     (conA : isConnected (suc n) A)
+     (hlevB : (a : A) → isOfHLevel n (B a))
+     (p : Σ[ a ∈ A ] (B a)) where
+  private
+    module m = elim (λ (tt : Unit) → fst p)
+    P : A → TypeOfHLevel ℓ' n
+    P a = B a , hlevB a
+    con* = isConnectedPoint n conA (fst p)
+
+  elim : (a : A) → B a
+  elim = Iso.inv (m.isIsoPrecompose n P con*) λ _ → snd p
+
+  β : elim (fst p) ≡ snd p
+  β = m.isIsoPrecomposeβ n P con* (λ _ → snd p) tt
+
 connectedTruncIso : ∀ {ℓ} {A B : Type ℓ} (n : HLevel) (f : A → B)
                    → isConnectedFun n f
                    → Iso (hLevelTrunc n A) (hLevelTrunc n B)
diff --git a/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda b/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda
index 31aa3fbd45..74733bfdb0 100644
--- a/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda
+++ b/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda
@@ -143,6 +143,31 @@ module _ {G'' : Ring ℓ} where
                               (fst TensorMultHom b) (fst TensorMultHom c)))
               λ x y ind ind2 → cong₂ _+G_ ind ind2))
 
+  EM→ΩEM+1-distr⌣ₖ0n : (n : ℕ)
+    → (x : EM G' zero) (y : EM G' (suc n))
+    → EM→ΩEM+1 (suc n) (_⌣ₖ_{n = zero} {m = suc n} x y)
+     ≡ λ i → _⌣ₖ_ {n = suc zero} {m = suc n} (EM→ΩEM+1 0 x i) y
+  EM→ΩEM+1-distr⌣ₖ0n n x y =
+      EMFun-EM→ΩEM+1 (suc n) _
+
+  EM→ΩEM+1-distr⌣ₖ0 : (n : ℕ)
+    → (x : EM G' (suc n)) (y : EM G' zero)
+    → EM→ΩEM+1 (suc n) (_⌣ₖ_{n = (suc n)} {m = zero} x y)
+     ≡ λ i → _⌣ₖ_ {n = suc (suc n)} {m = zero} (EM→ΩEM+1 (suc n) x i) y
+  EM→ΩEM+1-distr⌣ₖ0 n x y =
+     EMFun-EM→ΩEM+1 (suc n) (_⌣ₖ⊗_{n = (suc n)} {m = zero} x y)
+    ∙ cong (cong (inducedFun-EM TensorMultHom (suc (suc n))))
+           (EM→ΩEM+1-distrₙ₀ n y x)
+
+  EM→ΩEM+1-distr⌣ₖ : (n m : ℕ)
+    → (x : EM G' (suc n)) (y : EM G' (suc m))
+    → EM→ΩEM+1 (suc n +' suc m) (_⌣ₖ_{n = (suc n)} {m = suc m} x y)
+     ≡ λ i → _⌣ₖ_ {n = suc (suc n)} {m = suc m} (EM→ΩEM+1 (suc n) x i) y
+  EM→ΩEM+1-distr⌣ₖ n m x y =
+      EMFun-EM→ΩEM+1 _ (_⌣ₖ⊗_{n = (suc n)} {m = suc m} x y)
+    ∙ cong (cong (inducedFun-EM TensorMultHom (suc (suc n) +' suc m)))
+           (EM→ΩEM+1-distrₙsuc n m x y)
+
 -- graded commutativity
 module _ {G'' : CommRing ℓ} where
   private
@@ -198,7 +223,7 @@ module _ {G'' : CommRing ℓ} where
   → EM (Ring→AbGroup (CommRing→Ring R)) (n +' m)
 ⌣[,,]Cₖ-syntax n m R x y = x ⌣ₖ y
 
-syntax ⌣[]ₖ-syntax R x y = x ⌣[ R ]ₖ y
-syntax ⌣[]Cₖ-syntax R x y = x ⌣[ R ]Cₖ y
+syntax ⌣[]ₖ-syntax R x y = x ⌣[ R R]ₖ y
+syntax ⌣[]Cₖ-syntax R x y = x ⌣[ R R]Cₖ y
 syntax ⌣[,,]ₖ-syntax n m R x y = x ⌣[ R , n , m ]ₖ y
 syntax ⌣[,,]Cₖ-syntax n m R x y = x ⌣[ R , n , m ]Cₖ y
diff --git a/Cubical/Homotopy/EilenbergMacLane/GroupStructure.agda b/Cubical/Homotopy/EilenbergMacLane/GroupStructure.agda
index ee7ea93e32..3b75b6afe8 100644
--- a/Cubical/Homotopy/EilenbergMacLane/GroupStructure.agda
+++ b/Cubical/Homotopy/EilenbergMacLane/GroupStructure.agda
@@ -446,6 +446,16 @@ module _ {G : AbGroup ℓ} where
        ∙ sym (lUnit _)
        ◁ λ i j → ∣ compPath-filler (merid a) (sym (merid ptEM-raw)) (~ i) j ∣ₕ)
 
+_+ₖ∙_ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {G : AbGroup ℓ'} {n : ℕ}
+  → (A →∙ EM∙ G n) → (A →∙ EM∙ G n)
+  → A →∙ EM∙ G n
+fst (f +ₖ∙ g) x = fst f x +ₖ fst g x
+snd (_+ₖ∙_ {A = A} {n = n} f g) = s
+  where
+  abstract
+    s : fst f (pt A) +ₖ fst g (pt A) ≡ 0ₖ n
+    s = cong₂ _+ₖ_ (snd f) (snd g) ∙ rUnitₖ _ (0ₖ _)
+
 -distrₖ : {G : AbGroup ℓ} (n : ℕ) (x y : EM G n)
   → -[ n ]ₖ (x +[ n ]ₖ y) ≡ (-[ n ]ₖ x) +[ n ]ₖ (-[ n ]ₖ y)
 -distrₖ {G = G} zero x y =
diff --git a/Cubical/Homotopy/EilenbergMacLane/Order2.agda b/Cubical/Homotopy/EilenbergMacLane/Order2.agda
index f482decae5..bd09f17d52 100644
--- a/Cubical/Homotopy/EilenbergMacLane/Order2.agda
+++ b/Cubical/Homotopy/EilenbergMacLane/Order2.agda
@@ -247,7 +247,7 @@ symConst-ℤ/2-refl = EMZ/2.symConstEM-refl
    (evenOrOdd n)
 
 ⌣ₖ-commℤ/2 : (n m : ℕ) (x : EM ℤ/2 n) (y : EM ℤ/2 m)
-  → (x ⌣[ ℤ/2Ring ]ₖ y) ≡ subst (EM ℤ/2) (+'-comm m n) (y ⌣[ ℤ/2Ring ]ₖ x)
+  → (x ⌣[ ℤ/2Ring R]ₖ y) ≡ subst (EM ℤ/2) (+'-comm m n) (y ⌣[ ℤ/2Ring R]ₖ x)
 ⌣ₖ-commℤ/2 n m x y = ⌣ₖ-comm {G'' = ℤ/2CommRing} n m x y
                    ∙ cong (subst (EM ℤ/2) (+'-comm m n))
                       (-ₖ^[ n · m ]-const _)
diff --git a/Cubical/Homotopy/EilenbergMacLane/Properties.agda b/Cubical/Homotopy/EilenbergMacLane/Properties.agda
index c002976c3b..76a5092bec 100644
--- a/Cubical/Homotopy/EilenbergMacLane/Properties.agda
+++ b/Cubical/Homotopy/EilenbergMacLane/Properties.agda
@@ -438,6 +438,79 @@ module _ {G : AbGroup ℓ} where
   EM→ΩEM+1∘EM-raw→EM zero x = refl
   EM→ΩEM+1∘EM-raw→EM (suc n) x = refl
 
+  EM→ΩEM+1-gen : (n : ℕ) (x : EM G (suc n))
+    → EM G n → x ≡ x
+  EM→ΩEM+1-gen n x p =
+       sym (rUnitₖ (suc n) x)
+    ∙∙ cong (x +ₖ_) (EM→ΩEM+1 n p)
+    ∙∙ rUnitₖ (suc n) x
+
+  ΩEM+1-gen→EM-0ₖ : (n : ℕ) (x : _)
+    → ΩEM+1→EM-gen n (0ₖ (suc n)) x
+    ≡ ΩEM+1→EM n x
+  ΩEM+1-gen→EM-0ₖ zero p = refl
+  ΩEM+1-gen→EM-0ₖ (suc n) p = refl
+
+  EM→ΩEM+1-gen-0ₖ : (n : ℕ) (x : _)
+    → EM→ΩEM+1-gen n (0ₖ (suc n)) x
+    ≡ EM→ΩEM+1 n x
+  EM→ΩEM+1-gen-0ₖ zero x = sym (rUnit _)
+    ∙ λ j i → lUnitₖ 1 (EM→ΩEM+1 zero x i) j
+  EM→ΩEM+1-gen-0ₖ (suc n) x = sym (rUnit _)
+    ∙ λ j i → lUnitₖ (suc (suc n)) (EM→ΩEM+1 (suc n) x i) j
+
+  EM→ΩEM+1→EM-gen : (n : ℕ) (x : EM G (suc n))
+    → (y : EM G n) → ΩEM+1→EM-gen n x (EM→ΩEM+1-gen n x y) ≡ y
+  EM→ΩEM+1→EM-gen n =
+    EM-raw'-elim _ _
+      (λ _ → isOfHLevelΠ (suc (suc n))
+            (λ _ → isOfHLevelPath (suc (suc n))
+            (hLevelEM _ n) _ _))
+     (EM-raw'-trivElim _ n
+       (λ _ → isOfHLevelΠ (suc n) λ _ → hLevelEM _ n _ _)
+       λ y → cong (λ p → ΩEM+1→EM-gen n p
+                     (EM→ΩEM+1-gen n p y))
+              (EM-raw'→EM∙ G (suc n))
+            ∙ (λ i → ΩEM+1-gen→EM-0ₖ n (EM→ΩEM+1-gen-0ₖ n y i) i)
+            ∙ Iso.leftInv (Iso-EM-ΩEM+1 n) y)
+
+  ΩEM+1→EM→ΩEM+1-gen : (n : ℕ) (x : EM G (suc n))
+    → (y : x ≡ x) → EM→ΩEM+1-gen n x (ΩEM+1→EM-gen n x y) ≡ y
+  ΩEM+1→EM→ΩEM+1-gen n =
+    EM-raw'-elim _ _
+      (λ _ → isOfHLevelΠ (suc (suc n))
+              (λ _ → isOfHLevelPath (suc (suc n))
+              (hLevelEM _ (suc n) _ _) _ _))
+     (EM-raw'-trivElim _ n
+       (λ _ → isOfHLevelΠ (suc n)
+         λ _ → hLevelEM _ (suc n) _ _ _ _)
+     (subst (λ p → (y : p ≡ p)
+       → EM→ΩEM+1-gen n p (ΩEM+1→EM-gen n p y) ≡ y)
+       (sym (EM-raw'→EM∙ _ (suc n)))
+       λ p → (λ i → EM→ΩEM+1-gen-0ₖ n (ΩEM+1-gen→EM-0ₖ n p i) i)
+            ∙ Iso.rightInv (Iso-EM-ΩEM+1 n) p))
+
+  Iso-EM-ΩEM+1-gen : (n : ℕ) (x : EM G (suc n))
+    → Iso (EM G n) (x ≡ x)
+  Iso.fun (Iso-EM-ΩEM+1-gen n x) = EM→ΩEM+1-gen n x
+  Iso.inv (Iso-EM-ΩEM+1-gen n x) = ΩEM+1→EM-gen n x
+  Iso.rightInv (Iso-EM-ΩEM+1-gen n x) = ΩEM+1→EM→ΩEM+1-gen n x
+  Iso.leftInv (Iso-EM-ΩEM+1-gen n x) = EM→ΩEM+1→EM-gen n x
+
+  ΩEM+1→EM-gen-refl : (n : ℕ) (x : EM G (suc n))
+    → ΩEM+1→EM-gen n x refl ≡ 0ₖ n
+  ΩEM+1→EM-gen-refl n =
+    EM-raw'-elim _ (suc n)
+      (λ _ → isOfHLevelPath (suc (suc n)) (hLevelEM _ n) _ _)
+      (EM-raw'-trivElim _ n
+        (λ _ → hLevelEM _ n _ _)
+        (lem n))
+    where
+    lem : (n : ℕ) → ΩEM+1→EM-gen n
+      (EM-raw'→EM G (suc n) (snd (EM-raw'∙ G (suc n)))) refl
+      ≡ 0ₖ n
+    lem zero = ΩEM+1→EM-refl 0
+    lem (suc n) = ΩEM+1→EM-refl (suc n)
 
 -- Some HLevel lemmas about function spaces (EM∙ G n →∙ EM∙ H m), mainly used for
 -- the cup product
diff --git a/Cubical/Homotopy/Loopspace.agda b/Cubical/Homotopy/Loopspace.agda
index 05f722d1e4..b5b2d5aecd 100644
--- a/Cubical/Homotopy/Loopspace.agda
+++ b/Cubical/Homotopy/Loopspace.agda
@@ -209,6 +209,19 @@ snd (inv (ΩfunExtIso A B) (f , p) i) j = p j i
 rightInv (ΩfunExtIso A B) _ = refl
 leftInv (ΩfunExtIso A B) _ = refl
 
+relax→∙Ω-Iso : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
+  → Iso (Σ[ b ∈ fst B ] (fst A → b ≡ pt B))
+         (A →∙ (Ω B))
+Iso.fun (relax→∙Ω-Iso {A = A}) (b , p) = (λ a → sym (p (pt A)) ∙ p a) , lCancel (p (snd A))
+Iso.inv (relax→∙Ω-Iso {B = B}) a = (pt B) , (fst a)
+Iso.rightInv (relax→∙Ω-Iso) a =
+  →∙Homogeneous≡ (isHomogeneousPath _ _)
+    (funExt λ x → cong (_∙ fst a x) (cong sym (snd a)) ∙ sym (lUnit (fst a x)))
+Iso.leftInv (relax→∙Ω-Iso {A = A}) (b , p) =
+  ΣPathP (sym (p (pt A))
+       , λ i a j → compPath-filler' (sym (p (pt A))) (p a) (~ i) j)
+
+
 {- Commutativity of loop spaces -}
 isComm∙ : ∀ {ℓ} (A : Pointed ℓ) → Type ℓ
 isComm∙ A = (p q : typ (Ω A)) → p ∙ q ≡ q ∙ p