diff --git a/Cubical/Algebra/Group/Instances/IntMod.agda b/Cubical/Algebra/Group/Instances/IntMod.agda
index 95dc1bae3..b00e67551 100644
--- a/Cubical/Algebra/Group/Instances/IntMod.agda
+++ b/Cubical/Algebra/Group/Instances/IntMod.agda
@@ -207,5 +207,11 @@ isHomℤ→Fin n =
 ℤ/2-elim {A = A} a₀ a₁ (suc (suc x) , p) =
   ⊥.rec (snotz (cong (λ x → predℕ (predℕ x)) (+-comm (3 +ℕ x) (fst p) ∙ snd p)))
 
+ℤ/2-rec : ∀ {ℓ} {A : Type ℓ} → A → A → Fin 2 → A
+ℤ/2-rec {A = A} a₀ a₁ (zero , p) = a₀
+ℤ/2-rec {A = A} a₀ a₁ (suc zero , p) = a₁
+ℤ/2-rec {A = A} a₀ a₁ (suc (suc x) , p) =
+  ⊥.rec (snotz (cong (λ x → predℕ (predℕ x)) (+-comm (3 +ℕ x) (fst p) ∙ snd p)))
+
 -Const-ℤ/2 : (x : fst (ℤGroup/ 2)) → -ₘ x ≡ x
 -Const-ℤ/2 = ℤ/2-elim refl refl
diff --git a/Cubical/Cohomology/EilenbergMacLane/Base.agda b/Cubical/Cohomology/EilenbergMacLane/Base.agda
index 35a88025c..471611149 100644
--- a/Cubical/Cohomology/EilenbergMacLane/Base.agda
+++ b/Cubical/Cohomology/EilenbergMacLane/Base.agda
@@ -4,6 +4,7 @@ module Cubical.Cohomology.EilenbergMacLane.Base where
 
 open import Cubical.Homotopy.EilenbergMacLane.GroupStructure
 open import Cubical.Homotopy.EilenbergMacLane.Base
+open import Cubical.Homotopy.EilenbergMacLane.Order2
 
 open import Cubical.Foundations.Prelude
 
@@ -13,6 +14,7 @@ open import Cubical.Algebra.Group.Base
 open import Cubical.Algebra.AbGroup.Base
 open import Cubical.Algebra.Monoid
 open import Cubical.Algebra.Semigroup
+open import Cubical.Algebra.Group.Instances.IntMod
 
 open import Cubical.HITs.SetTruncation as ST
   hiding (rec ; map ; elim ; elim2 ; elim3)
@@ -96,3 +98,18 @@ is-set (isSemigroup (isMonoid (isGroup (isAbGroup (snd (coHomGr n G A)))))) = sq
 ·InvR (isGroup (isAbGroup (snd (coHomGr n G A)))) = rCancelₕ n
 ·InvL (isGroup (isAbGroup (snd (coHomGr n G A)))) = lCancelₕ n
 +Comm (isAbGroup (snd (coHomGr n G A))) = commₕ n
+
+
+-- ℤ/2 lemmas
++ₕ≡id-ℤ/2 : ∀ {ℓ}  {A : Type ℓ} (n : ℕ) (x : coHom n ℤ/2 A) → x +ₕ x ≡ 0ₕ n
++ₕ≡id-ℤ/2 n =
+  ST.elim (λ _ → isSetPathImplicit)
+    λ f → cong ∣_∣₂ (funExt λ x → +ₖ≡id-ℤ/2 n (f x))
+
+-ₕConst-ℤ/2 : ∀{ℓ} (n : ℕ) {A : Type ℓ} (x : coHom n ℤ/2 A) → -ₕ x ≡ x
+-ₕConst-ℤ/2 zero =
+  ST.elim (λ _ → isSetPathImplicit)
+    λ f → cong ∣_∣₂ (funExt λ x → -Const-ℤ/2 (f x))
+-ₕConst-ℤ/2 (suc n) =
+  ST.elim (λ _ → isSetPathImplicit)
+    λ f → cong ∣_∣₂ (funExt λ x → -ₖConst-ℤ/2 n (f x))
diff --git a/Cubical/Cohomology/EilenbergMacLane/CupProduct.agda b/Cubical/Cohomology/EilenbergMacLane/CupProduct.agda
index 16a5dae43..a3da03ee5 100644
--- a/Cubical/Cohomology/EilenbergMacLane/CupProduct.agda
+++ b/Cubical/Cohomology/EilenbergMacLane/CupProduct.agda
@@ -14,6 +14,7 @@ open import Cubical.Algebra.Ring
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Transport
 
 open import Cubical.HITs.EilenbergMacLane1
 open import Cubical.HITs.SetTruncation as ST
@@ -93,3 +94,19 @@ module _ {G'' : Ring ℓ} {A : Type ℓ'} where
           λ h → cong ∣_∣₂ (funExt λ x → assoc⌣ₖ n m l (f x) (g x) (h x)
             ∙ cong (transport (λ i → EM G' (+'-assoc n m l i)))
                (cong (λ x → (f x ⌣ₖ (g x ⌣ₖ h x))) (sym (transportRefl x))))
+
+-- dependent versions
+module _ {G'' : Ring ℓ} {A : Type ℓ'} where
+  private
+    G' = Ring→AbGroup G''
+
+  ⌣-1ₕDep : (n : ℕ) (x : coHom n G' A)
+    → PathP (λ i → coHom (+'-comm zero n (~ i)) G' A) (x ⌣ 1ₕ) x
+  ⌣-1ₕDep n x = toPathP {A = λ i → coHom (+'-comm zero n (~ i)) G' A}
+                        (flipTransport (⌣-1ₕ n x))
+
+  assoc⌣Dep : (n m l : ℕ)
+       (x : coHom n G' A) (y : coHom m G' A) (z : coHom l G' A)
+    → PathP (λ i → coHom (+'-assoc n m l (~ i)) G' A) ((x ⌣ y) ⌣ z) (x ⌣ (y ⌣ z))
+  assoc⌣Dep n m l x y z = toPathP {A = λ i → coHom (+'-assoc n m l (~ i)) G' A}
+                                  (flipTransport (assoc⌣ n m l x y z))
diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/KleinBottle.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/KleinBottle.agda
index 8520f11ac..70270bc35 100644
--- a/Cubical/Cohomology/EilenbergMacLane/Groups/KleinBottle.agda
+++ b/Cubical/Cohomology/EilenbergMacLane/Groups/KleinBottle.agda
@@ -335,26 +335,27 @@ snd H²[K²,ℤ/2]≅ℤ/2 =
         (ℤ/2-elim (IsAbGroup.+IdR e 1)
           (IsAbGroup.+InvR e 1))))
 
+isContr-HⁿKleinBottle : (n : ℕ) (G : AbGroup ℓ)
+  → isContr (coHom (suc (suc (suc n))) G KleinBottle)
+fst (isContr-HⁿKleinBottle n G) = ∣ (KleinFun ∣ north ∣ refl refl refl) ∣₂
+snd (isContr-HⁿKleinBottle n G) = ST.elim (λ _ → isSetPathImplicit)
+         (ConnK².elim₂ (isConnectedSubtr 3 (suc n)
+           (subst (λ m → isConnected m (EM G (3 +ℕ n)))
+             (cong suc (+-comm 3 n))
+             (isConnectedEM (3 +ℕ n)))) (λ _ → squash₂ _ _)
+            (0ₖ (3 +ℕ n))
+            λ p → TR.rec (squash₂ _ _)
+              (λ q → cong ∣_∣₂ (cong (KleinFun ∣ north ∣ refl refl) q))
+              (isConnectedPath 1
+                (isConnectedPath 2
+                  (isConnectedPath 3
+                    ((isConnectedSubtr 4 n
+                     (subst (λ m → isConnected m (EM G (3 +ℕ n)))
+                       (+-comm 4 n)
+                       (isConnectedEM (3 +ℕ n))))) _ _) _ _)
+                         refl p .fst))
+
 H³⁺ⁿK²≅0 : (n : ℕ) (G : AbGroup ℓ)
   → AbGroupEquiv (coHomGr (3 +ℕ n) G KleinBottle) (trivialAbGroup {ℓ})
-fst (H³⁺ⁿK²≅0 n G) = isContr→Equiv lem isContrUnit*
-  where
-  lem : isContr (coHom (suc (suc (suc n))) G KleinBottle)
-  fst lem = ∣ (KleinFun ∣ north ∣ refl refl refl) ∣₂
-  snd lem = ST.elim (λ _ → isSetPathImplicit)
-           (ConnK².elim₂ (isConnectedSubtr 3 (suc n)
-             (subst (λ m → isConnected m (EM G (3 +ℕ n)))
-               (cong suc (+-comm 3 n))
-               (isConnectedEM (3 +ℕ n)))) (λ _ → squash₂ _ _)
-              (0ₖ (3 +ℕ n))
-              λ p → TR.rec (squash₂ _ _)
-                (λ q → cong ∣_∣₂ (cong (KleinFun ∣ north ∣ refl refl) q))
-                (isConnectedPath 1
-                  (isConnectedPath 2
-                    (isConnectedPath 3
-                      ((isConnectedSubtr 4 n
-                       (subst (λ m → isConnected m (EM G (3 +ℕ n)))
-                         (+-comm 4 n)
-                         (isConnectedEM (3 +ℕ n))))) _ _) _ _)
-                           refl p .fst))
+fst (H³⁺ⁿK²≅0 n G) = isContr→Equiv (isContr-HⁿKleinBottle n G) isContrUnit*
 snd (H³⁺ⁿK²≅0 n G) = makeIsGroupHom λ _ _ → refl
diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/Wedge.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/Wedge.agda
new file mode 100644
index 000000000..08a8e630d
--- /dev/null
+++ b/Cubical/Cohomology/EilenbergMacLane/Groups/Wedge.agda
@@ -0,0 +1,128 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Cohomology.EilenbergMacLane.Groups.Wedge where
+
+open import Cubical.Cohomology.EilenbergMacLane.Base
+
+open import Cubical.Homotopy.EilenbergMacLane.Base
+open import Cubical.Homotopy.EilenbergMacLane.GroupStructure
+open import Cubical.Homotopy.EilenbergMacLane.Properties
+open import Cubical.Homotopy.Connected
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Function
+
+open import Cubical.Data.Nat
+open import Cubical.Data.Sigma
+
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Properties
+open import Cubical.Algebra.AbGroup.Base
+
+open import Cubical.HITs.SetTruncation as ST
+open import Cubical.HITs.Truncation as Trunc
+open import Cubical.HITs.Pushout
+open import Cubical.HITs.Wedge
+
+open import Cubical.Foundations.HLevels
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module _ {A : Pointed ℓ} {B : Pointed ℓ'} (G : AbGroup ℓ) where
+  A∨B = A ⋁ B
+
+  open AbGroupStr (snd G) renaming (_+_ to _+G_ ; -_ to -G_)
+
+  private
+    ×H : (n : ℕ) → AbGroup _
+    ×H n = dirProdAb (coHomGr (suc n) G (fst A))
+                     (coHomGr (suc n) G (fst B))
+
+  Hⁿ×→Hⁿ-⋁ : (n : ℕ) → (A ⋁ B → EM G (suc n))
+    → (fst A → EM G (suc n)) × (fst B → EM G (suc n))
+  fst (Hⁿ×→Hⁿ-⋁ n f) x = f (inl x)
+  snd (Hⁿ×→Hⁿ-⋁ n f) x = f (inr x)
+
+  Hⁿ-⋁→Hⁿ× : (n : ℕ)
+    → (f : fst A → EM G (suc n))
+    → (g : fst B → EM G (suc n))
+    → (A ⋁ B → EM G (suc n))
+  Hⁿ-⋁→Hⁿ× n f g (inl x) = f x -[ (suc n) ]ₖ f (pt A)
+  Hⁿ-⋁→Hⁿ× n f g (inr x) = g x -[ (suc n) ]ₖ g (pt B)
+  Hⁿ-⋁→Hⁿ× n f g (push a i) =
+    (rCancelₖ (suc n) (f (pt A)) ∙ sym (rCancelₖ (suc n) (g (pt B)))) i
+
+  Hⁿ⋁-Iso : (n : ℕ)
+    → Iso (coHom (suc n) G (A ⋁ B))
+           (coHom (suc n) G (fst A)
+          × coHom (suc n) G (fst B))
+  Iso.fun (Hⁿ⋁-Iso n) =
+    ST.rec (isSet× squash₂ squash₂)
+      λ f → ∣ f ∘ inl ∣₂ , ∣ f ∘ inr ∣₂
+  Iso.inv (Hⁿ⋁-Iso n) =
+    uncurry (ST.rec2 squash₂ λ f g → ∣ Hⁿ-⋁→Hⁿ× n f g ∣₂)
+  Iso.rightInv (Hⁿ⋁-Iso n) =
+    uncurry (ST.elim2
+      (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _)
+      λ f g
+      → ΣPathP (Trunc.rec (isProp→isOfHLevelSuc n (squash₂ _ _))
+                (λ p → cong ∣_∣₂ (funExt λ x → cong (λ z → f x +[ (suc n) ]ₖ z)
+                                 (cong (λ z → -[ (suc n) ]ₖ z) p ∙ -0ₖ (suc n))
+                              ∙ rUnitₖ (suc n) (f x)))
+              (isConnectedPath (suc n)
+               (isConnectedEM (suc n)) (f (pt A)) (0ₖ (suc n)) .fst)
+            , Trunc.rec (isProp→isOfHLevelSuc n (squash₂ _ _))
+                (λ p → cong ∣_∣₂ (funExt λ x → cong (λ z → g x +[ (suc n) ]ₖ z)
+                                 (cong (λ z → -[ (suc n) ]ₖ z) p ∙ -0ₖ (suc n))
+                              ∙ rUnitₖ (suc n) (g x)))
+              (isConnectedPath (suc n)
+               (isConnectedEM (suc n)) (g (pt B)) (0ₖ (suc n)) .fst)))
+  Iso.leftInv (Hⁿ⋁-Iso n) =
+    ST.elim (λ _ → isSetPathImplicit)
+      λ f → Trunc.rec (isProp→isOfHLevelSuc n (squash₂ _ _))
+        (λ p → cong ∣_∣₂
+          (funExt λ { (inl x) → pgen f p (inl x)
+                    ; (inr x) → p₂ f p x
+                    ; (push a i) j → Sq f p j i}))
+        (Iso.fun (PathIdTruncIso (suc n))
+          (isContr→isProp (isConnectedEM {G' = G}  (suc n))
+            ∣ f (inl (pt A)) ∣ ∣ 0ₖ (suc n) ∣ ))
+    where
+    module _ (f : (A ⋁ B → EM G (suc n))) (p : f (inl (pt A)) ≡ 0ₖ (suc n))
+      where
+      pgen : (x : A ⋁ B) → _ ≡ _
+      pgen x =
+          (λ j → f x -[ (suc n) ]ₖ (p j))
+       ∙∙ (λ j → f x +[ (suc n) ]ₖ (-0ₖ (suc n) j))
+       ∙∙ rUnitₖ (suc n) (f x)
+
+      p₂ : (x : typ B) → _ ≡ _
+      p₂ x = (λ j → f (inr x) -[ (suc n) ]ₖ (f (sym (push tt) j)))
+            ∙ pgen (inr x)
+
+
+      Sq : Square (rCancelₖ (suc n) (f (inl (pt A)))
+                    ∙ sym (rCancelₖ (suc n) (f (inr (pt B)))))
+                   (cong f (push tt))
+                   (pgen (inl (pt A)))
+                   (p₂ (pt B))
+      Sq i j =
+        hcomp (λ k → λ {(i = i0) → (rCancelₖ (suc n) (f (inl (pt A)))
+                                   ∙ sym (rCancelₖ (suc n) (f (push tt k)))) j
+                       ; (i = i1) → f (push tt (k ∧ j))
+                       ; (j = i0) → pgen (inl (pt A)) i
+                       ; (j = i1) → ((λ j → f (push tt k) -[ (suc n) ]ₖ
+                                             (f (sym (push tt) (j ∨ ~ k))))
+                                    ∙ pgen (push tt k)) i})
+         (hcomp (λ k → λ {(i = i0) → rCancel (rCancelₖ (suc n)
+                                               (f (inl (pt A)))) (~ k) j
+                         ; (i = i1) → f (inl (pt A))
+                         ; (j = i0) → pgen (inl (pt A)) i
+                         ; (j = i1) → lUnit (pgen (inl (pt A))) k i})
+                (pgen (inl (pt A)) i))
diff --git a/Cubical/Cohomology/EilenbergMacLane/RingStructure.agda b/Cubical/Cohomology/EilenbergMacLane/RingStructure.agda
new file mode 100644
index 000000000..461e19f78
--- /dev/null
+++ b/Cubical/Cohomology/EilenbergMacLane/RingStructure.agda
@@ -0,0 +1,187 @@
+{-# OPTIONS --safe --experimental-lossy-unification #-}
+module Cubical.Cohomology.EilenbergMacLane.RingStructure where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Transport
+
+open import Cubical.Data.Nat renaming (_+_ to _+n_ ; _·_ to _·n_)
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum
+
+open import Cubical.Algebra.Monoid
+open import Cubical.Algebra.Monoid.Instances.NatPlusBis
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.AbGroup
+open import Cubical.Algebra.Ring
+open import Cubical.Algebra.GradedRing.DirectSumHIT
+
+open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
+open import Cubical.Algebra.AbGroup.Instances.DirectSumHIT
+
+open import Cubical.HITs.SetTruncation as ST
+
+open import Cubical.Cohomology.EilenbergMacLane.Base
+open import Cubical.Cohomology.EilenbergMacLane.CupProduct
+
+private variable
+  ℓ ℓ' ℓ'' : Level
+
+open Iso
+
+-----------------------------------------------------------------------------
+-- Definition Cohomology Ring
+
+open PlusBis
+open GradedRing-⊕HIT-index
+open GradedRing-⊕HIT-⋆
+open RingStr
+
+
+module _ (R : Ring ℓ') (A : Type ℓ) where
+  private
+    R-ab = Ring→AbGroup R
+
+  H*R : Ring _
+  H*R = ⊕HITgradedRing-Ring
+        NatPlusBis-Monoid
+        (λ k → coHom k R-ab A)
+        (λ k → snd (coHomGr k R-ab A))
+        1ₕ
+        _⌣_
+        (λ {k} {l} → 0ₕ-⌣ k l)
+        (λ {k} {l} → ⌣-0ₕ k l)
+        (λ _ _ _ → sym (ΣPathTransport→PathΣ _ _ (sym (+'-assoc _ _ _) , flipTransport (assoc⌣ _ _ _ _ _ _))))
+        (λ {n} a → sym (ΣPathTransport→PathΣ _ _ (sym (+'-rid _)
+                  , sym (⌣-1ₕ _ _ ∙ cong (λ p → subst (λ p → coHom p R-ab A) p a)
+                        (isSetℕ _ _ _ _)))))
+        (λ _ → ΣPathTransport→PathΣ _ _ (refl , transportRefl _ ∙ 1ₕ-⌣ _ _))
+        (λ _ _ _ → distrL⌣ _ _ _ _ _)
+        λ _ _ _ → distrR⌣ _ _ _ _ _
+
+  H* : Type _
+  H* = fst H*R
+
+module CohomologyRing-Equiv
+  {R : Ring ℓ}
+  {X : Type ℓ'}
+  {Y : Type ℓ''}
+  (e : Iso X Y)
+  where
+  private
+    R-ab = Ring→AbGroup R
+
+  open IsGroupHom
+
+  open RingStr (snd (H*R R X)) using ()
+    renaming
+    ( 0r        to 0H*X
+    ; 1r        to 1H*X
+    ; _+_       to _+H*X_
+    ; -_        to -H*X_
+    ; _·_       to _cupX_
+    ; +Assoc    to +H*XAssoc
+    ; +IdR      to +H*XIdR
+    ; +Comm     to +H*XComm
+    ; ·Assoc    to ·H*XAssoc
+    ; is-set    to isSetH*X     )
+
+  open RingStr (snd (H*R R Y)) using ()
+    renaming
+    ( 0r        to 0H*Y
+    ; 1r        to 1H*Y
+    ; _+_       to _+H*Y_
+    ; -_        to -H*Y_
+    ; _·_       to _cupY_
+    ; +Assoc    to +H*YAssoc
+    ; +IdR      to +H*YIdR
+    ; +Comm     to +H*YComm
+    ; ·Assoc    to ·H*YAssoc
+    ; is-set    to isSetH*Y     )
+
+
+  coHomGr-Iso : {n : ℕ} → AbGroupIso (coHomGr n R-ab X) (coHomGr n R-ab Y)
+  fst (coHomGr-Iso {n}) = is
+    where
+    is : Iso (coHom n R-ab X) (coHom n R-ab Y)
+    fun is = ST.rec squash₂ (λ f → ∣ (λ y → f (inv e y)) ∣₂)
+    inv is = ST.rec squash₂ (λ g → ∣ (λ x → g (fun e x)) ∣₂)
+    rightInv is = ST.elim (λ _ → isProp→isSet (squash₂ _ _)) (λ f → cong ∣_∣₂ (funExt (λ y → cong f (rightInv e y))))
+    leftInv is = ST.elim (λ _ → isProp→isSet (squash₂ _ _)) (λ g → cong ∣_∣₂ (funExt (λ x → cong g (leftInv e x))))
+  snd (coHomGr-Iso {n}) = makeIsGroupHom
+                                        (ST.elim (λ _ → isProp→isSet λ u v i y → squash₂ _ _ (u y) (v y) i)
+                                        (λ f → ST.elim (λ _ → isProp→isSet (squash₂ _ _))
+                                        (λ f' → refl)))
+
+  H*-X→H*-Y : H* R X → H* R Y
+  H*-X→H*-Y = DS-Rec-Set.f _ _ _ _ isSetH*Y
+               0H*Y
+               (λ n a → base n (fun (fst coHomGr-Iso) a))
+               _+H*Y_
+               +H*YAssoc
+               +H*YIdR
+               +H*YComm
+               (λ n → cong (base n) (pres1 (snd coHomGr-Iso)) ∙ base-neutral n)
+               λ n a b → base-add _ _ _ ∙ cong (base n) (sym (pres· (snd coHomGr-Iso) a b))
+
+  H*-Y→H*-X : H* R Y → H* R X
+  H*-Y→H*-X = DS-Rec-Set.f _ _ _ _ isSetH*X
+               0H*X
+               (λ m a → base m (inv (fst coHomGr-Iso) a))
+               _+H*X_
+               +H*XAssoc
+               +H*XIdR
+               +H*XComm
+               (λ m → cong (base m) (pres1 (snd (invGroupIso coHomGr-Iso))) ∙ base-neutral m)
+               λ m a b → base-add _ _ _ ∙ cong (base m) (sym (pres· (snd (invGroupIso coHomGr-Iso)) a b))
+
+  e-sect : (y : H* R Y) → H*-X→H*-Y (H*-Y→H*-X y) ≡ y
+  e-sect = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*Y _ _)
+           refl
+           (λ m a → cong (base m) (rightInv (fst coHomGr-Iso) a))
+           (λ {U V} ind-U ind-V → cong₂ _+H*Y_ ind-U ind-V)
+
+  e-retr : (x : H* R X) → H*-Y→H*-X (H*-X→H*-Y x) ≡ x
+  e-retr = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*X _ _)
+           refl
+           (λ n a → cong (base n) (leftInv (fst coHomGr-Iso) a))
+           (λ {U V} ind-U ind-V → cong₂ _+H*X_ ind-U ind-V)
+
+  H*-X→H*-Y-pres1 : H*-X→H*-Y 1H*X ≡ 1H*Y
+  H*-X→H*-Y-pres1 = refl
+
+  H*-X→H*-Y-pres+ : (x x' : H* R X) → H*-X→H*-Y (x +H*X x') ≡ H*-X→H*-Y x +H*Y H*-X→H*-Y x'
+  H*-X→H*-Y-pres+ x x' = refl
+
+  H*-X→H*-Y-pres· : (x x' : H* R X) → H*-X→H*-Y (x cupX x') ≡ H*-X→H*-Y x cupY H*-X→H*-Y x'
+  H*-X→H*-Y-pres· = DS-Ind-Prop.f _ _ _ _ (λ x u v i y → isSetH*Y _ _ (u y) (v y) i)
+         (λ _ → refl)
+         (λ n → ST.elim (λ x → isProp→isSet λ u v i y → isSetH*Y _ _ (u y) (v y) i)
+                (λ f → DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*Y _ _)
+                        refl
+                        (λ m → ST.elim (λ _ → isProp→isSet (isSetH*Y _ _))
+                                (λ g → refl))
+                        λ {U V} ind-U ind-V → cong₂ _+H*Y_ ind-U ind-V) )
+         (λ {U V} ind-U ind-V y → cong₂ _+H*Y_ (ind-U y) (ind-V y))
+
+
+module _
+  {R : Ring ℓ}
+  {X : Type ℓ'}
+  {Y : Type ℓ''}
+  (e : Iso X Y)
+  where
+
+  open CohomologyRing-Equiv {R = R} e
+  CohomologyRing-Equiv : RingEquiv (H*R R X) (H*R R Y)
+  fst CohomologyRing-Equiv = isoToEquiv is
+    where
+    is : Iso (H* R X) (H* R Y)
+    fun is = H*-X→H*-Y
+    inv is = H*-Y→H*-X
+    rightInv is = e-sect
+    leftInv is = e-retr
+  snd CohomologyRing-Equiv =
+    makeIsRingHom H*-X→H*-Y-pres1 H*-X→H*-Y-pres+ H*-X→H*-Y-pres·
diff --git a/Cubical/Cohomology/EilenbergMacLane/Rings/KleinBottle.agda b/Cubical/Cohomology/EilenbergMacLane/Rings/KleinBottle.agda
index b861e2237..116dfc14e 100644
--- a/Cubical/Cohomology/EilenbergMacLane/Rings/KleinBottle.agda
+++ b/Cubical/Cohomology/EilenbergMacLane/Rings/KleinBottle.agda
@@ -5,9 +5,11 @@ module Cubical.Cohomology.EilenbergMacLane.Rings.KleinBottle where
 open import Cubical.Cohomology.EilenbergMacLane.Groups.KleinBottle
 open import Cubical.Cohomology.EilenbergMacLane.Base
 open import Cubical.Cohomology.EilenbergMacLane.CupProduct
+open import Cubical.Cohomology.EilenbergMacLane.RingStructure
 
 open import Cubical.Homotopy.EilenbergMacLane.Properties
 open import Cubical.Homotopy.EilenbergMacLane.Base
+open import Cubical.Homotopy.EilenbergMacLane.GroupStructure
 open import Cubical.Homotopy.EilenbergMacLane.Order2
 open import Cubical.Homotopy.EilenbergMacLane.CupProduct
 open import Cubical.Homotopy.EilenbergMacLane.CupProductTensor
@@ -16,27 +18,47 @@ open import Cubical.Homotopy.Loopspace
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Function
 open import Cubical.Foundations.Path
 open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Transport
+open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.Pointed.Homogeneous
+open import Cubical.Foundations.Equiv
 
 open import Cubical.Data.Nat
 open import Cubical.Data.Fin
+open import Cubical.Data.Fin.Arithmetic
+open import Cubical.Data.FinData
+open import Cubical.Data.Vec
+open import Cubical.Data.Sigma
 
-open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
 open import Cubical.Algebra.Group.Instances.IntMod
 open import Cubical.Algebra.AbGroup.Base
+open import Cubical.Algebra.CommRing.Base
 open import Cubical.Algebra.CommRing.Instances.IntMod
+open import Cubical.Algebra.CommRing.QuotientRing
+open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly
+open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly-Quotient
 open import Cubical.Algebra.AbGroup.TensorProduct
 open import Cubical.Algebra.Ring
+open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
 
 open import Cubical.HITs.KleinBottle renaming (rec to KleinFun)
 open import Cubical.HITs.EilenbergMacLane1
-open import Cubical.HITs.SetTruncation as ST
 open import Cubical.HITs.Truncation
+open import Cubical.HITs.SetTruncation as ST
+open import Cubical.HITs.PropositionalTruncation as PT
+open import Cubical.HITs.SetQuotients as SQ renaming (_/_ to _/sq_)
 open import Cubical.HITs.Susp
 
+open PlusBis
+open Iso
+
 private
   K[ℤ₂⊗ℤ₂,2] = EM (ℤ/2 ⨂ ℤ/2) 2
   K∙[ℤ₂⊗ℤ₂,2] = EM∙ (ℤ/2 ⨂ ℤ/2) 2
@@ -383,8 +405,8 @@ KleinFun-EMTensorMult-const (line2 i) = refl
 KleinFun-EMTensorMult-const (square i j) = refl
 
 
-lem2 : ℤ/2→Ω²K₂ 1 ≡ ℤ/2→Ω²K₂' 1
-lem2 k i j =
+ℤ/2→Ω²K₂'≡ : ℤ/2→Ω²K₂ 1 ≡ ℤ/2→Ω²K₂' 1
+ℤ/2→Ω²K₂'≡ k i j =
   hcomp (λ r → λ {(i = i0) → transportRefl (EM→ΩEM+1-0ₖ 1) k r j
                  ; (i = i1) → transportRefl (EM→ΩEM+1-0ₖ 1) k r j
                  ; (j = i0) → ∣ north ∣
@@ -451,6 +473,48 @@ module _ where
     ST.elim2 (λ _ _ → isSetPathImplicit)
      λ f g → cong ∣_∣₂ (funExt λ x → ⌣ₖ-commℤ/2₁,₁ (f x) (g x))
 
+  ⌣ₖ⊗-commℤ/2-base : (n : ℕ) (x : ℤ/2 .fst) (y : EM ℤ/2 n)
+    → PathP (λ i → EM ℤ/2 (PlusBis.+'-comm 0 n i))
+             (_⌣ₖ_ {G'' = ℤ/2Ring} {n = zero} {m = n} x y)
+             (_⌣ₖ_ {G'' = ℤ/2Ring} {n = n} {m = zero} y x)
+  ⌣ₖ⊗-commℤ/2-base n =
+      ℤ/2-elim (λ y → 0ₖ-⌣ₖ 0 n y
+             ◁ ((λ i → 0ₖ (PlusBis.+'-comm 0 n i))
+             ▷ sym (⌣ₖ-0ₖ n 0 y)))
+               (λ y → 1ₖ-⌣ₖ n y
+               ◁ (λ i → transp (λ j →  EM ℤ/2 (PlusBis.+'-comm 0 n (i ∧ j)))
+                                (~ i) y)
+               ▷ sym (⌣ₖ-1ₖ n y))
+
+⌣-comm-Klein : (n m : ℕ)
+  (x : coHom n ℤ/2 KleinBottle) (y : coHom m ℤ/2 KleinBottle)
+  → PathP (λ i → coHom (PlusBis.+'-comm n m i) ℤ/2 KleinBottle)
+           (_⌣_ {G'' = ℤ/2Ring} x y)
+           (_⌣_ {G'' = ℤ/2Ring} y x)
+⌣-comm-Klein zero m =
+  ST.elim2 (λ _ _ → isOfHLevelPathP 2 squash₂ _ _ )
+    λ f g i → ∣ (λ x → ⌣ₖ⊗-commℤ/2-base m (f x) (g x) i) ∣₂
+⌣-comm-Klein (suc n) zero x y =
+  transport (λ j → PathP
+      (λ i → coHom (isSetℕ _ _
+        (sym (PlusBis.+'-comm zero (suc n)))
+        (PlusBis.+'-comm (suc n) zero) j i) ℤ/2 KleinBottle)
+      (_⌣_ {G'' = ℤ/2Ring} x y) (_⌣_ {G'' = ℤ/2Ring} y x))
+      λ i → ⌣-comm-Klein zero (suc n) y x (~ i)
+⌣-comm-Klein (suc zero) (suc zero) = ⌣-commℤ/2₁,₁
+⌣-comm-Klein (suc zero) (suc (suc m)) x y =
+  isProp→PathP
+    (λ j → isContr→isProp
+      (transport (λ i → isContr (coHom
+        (PlusBis.+'-comm 1 (suc (suc m)) (j ∧ i)) ℤ/2 KleinBottle))
+        (isContr-HⁿKleinBottle m ℤ/2))) _ _
+⌣-comm-Klein (suc (suc n)) (suc m) x y =
+  isProp→PathP
+    (λ j → isContr→isProp
+      (transport (λ i → isContr (coHom
+        (PlusBis.+'-comm (suc (suc n)) (suc m) (i ∧ j)) ℤ/2 KleinBottle))
+        (isContr-HⁿKleinBottle _ ℤ/2))) _ _
+
 ------ Main results ------
 α↦1 : H¹K²→ℤ/2×ℤ/2 K²gen.α ≡ (1 , 0)
 α↦1 = refl
@@ -468,14 +532,14 @@ module _ where
                (KleinFun-α⊗ x ∙ KleinFun-ℤ/2→Ω²K₂⨂ x)
           ∙∙ KleinFun-EMTensorMult x
           ∙∙ sym (KleinFun-ℤ/2→Ω²K₂' x)
-           ∙ λ i → KleinFun (0ₖ 2) refl refl (lem2 (~ i)) x
+           ∙ λ i → KleinFun (0ₖ 2) refl refl (ℤ/2→Ω²K₂'≡ (~ i)) x
 
   cupIdα : _⌣_ {G'' = ℤ/2Ring} {n = 1} {m = 1} K²gen.α K²gen.α
          ≡ ℤ/2→H²K² 1
   cupIdα = cong ∣_∣₂ (funExt almostα)
 
-β²↦1 : H²K²→ℤ/2 (_⌣_ {G'' = ℤ/2Ring} {n = 1} {m = 1} K²gen.β K²gen.β) ≡ 0
-β²↦1 = cong H²K²→ℤ/2 cupIdΒ ∙ ℤ/2→H²K²→ℤ/2 0
+β²↦0 : H²K²→ℤ/2 (_⌣_ {G'' = ℤ/2Ring} {n = 1} {m = 1} K²gen.β K²gen.β) ≡ 0
+β²↦0 = cong H²K²→ℤ/2 cupIdΒ ∙ ℤ/2→H²K²→ℤ/2 0
   where
   ℤ/2→Ω²K₂-refl : ℤ/2→Ω²K₂ 0 ≡ refl
   ℤ/2→Ω²K₂-refl = Iso.leftInv Iso-Ω²K₂-ℤ/2 refl
@@ -493,8 +557,606 @@ module _ where
     (λ x → cong (EMTensorMult {G'' = ℤ/2Ring} 2)
              (KleinFun-βα⊗ x ∙ KleinFun-ℤ/2→Ω²K₂⨂ x)
         ∙∙ (KleinFun-EMTensorMult x  ∙ sym (KleinFun-ℤ/2→Ω²K₂' x))
-        ∙∙ λ i → KleinFun ∣ north ∣ refl refl (lem2 (~ i)) x)))
+        ∙∙ λ i → KleinFun ∣ north ∣ refl refl (ℤ/2→Ω²K₂'≡ (~ i)) x)))
       ∙ ℤ/2→H²K²→ℤ/2 1
 
 αβ↦1 : H²K²→ℤ/2 (_⌣_ {G'' = ℤ/2Ring} {n = 1} {m = 1} K²gen.α K²gen.β) ≡ 1
 αβ↦1 = cong H²K²→ℤ/2 (⌣-commℤ/2₁,₁ K²gen.α K²gen.β) ∙ βα↦1
+
+--------- Part 2: Show H*(K²,ℤ/2) ≅ ℤ/2[X,Y]/<X³,Y²,XY+X²> ----------
+
+-- some abbreviations
+open RingStr renaming (_+_ to _+r_ ; _·_ to _·r_)
+private
+   ℤ/2[X,Y] : CommRing ℓ-zero
+   ℤ/2[X,Y] = PolyCommRing ℤ/2CommRing 2
+
+   ℤ/2[X,Y]R = CommRing→Ring ℤ/2[X,Y]
+
+   -Z/2 = -_ (snd ℤ/2[X,Y]R)
+   _·Z/2_ = _·r_ (snd ℤ/2[X,Y]R)
+
+   _⌣'_ = _·r_ (snd (H*R ℤ/2Ring KleinBottle))
+
+   α⌣α = _⌣_ {G'' = ℤ/2Ring} K²gen.α K²gen.α
+   α⌣β = _⌣_ {G'' = ℤ/2Ring} K²gen.α K²gen.β
+
+-- Some abstract stuff for faster type checking
+abstract
+  H²[K²,ℤ/2]≅ℤ/2* : AbGroupEquiv (coHomGr 2 ℤ/2 KleinBottle) ℤ/2
+  H²[K²,ℤ/2]≅ℤ/2* = H²[K²,ℤ/2]≅ℤ/2
+
+  H²[K²,ℤ/2]≅ℤ/2*≡ : H²[K²,ℤ/2]≅ℤ/2* ≡ H²[K²,ℤ/2]≅ℤ/2
+  H²[K²,ℤ/2]≅ℤ/2*≡ = refl
+
+  α²↦1' : fst (fst (H²[K²,ℤ/2]≅ℤ/2*)) α⌣α ≡ 1
+  α²↦1' = α²↦1
+
+  αβ↦1' : fst (fst (H²[K²,ℤ/2]≅ℤ/2*)) α⌣β ≡ 1
+  αβ↦1' = αβ↦1
+
+
+
+-- some lemmas
+module _ where
+  -≡id-ℤ/2[X,Y] : (x : fst ℤ/2[X,Y]) → -Z/2 x ≡ x
+  -≡id-ℤ/2[X,Y] = DS-Ind-Prop.f _ _ _ _
+    (λ _ → is-set (snd ℤ/2[X,Y]R) _ _)
+    refl
+    (λ r a → cong (base r) (-Const-ℤ/2  _))
+    λ {x} {y} p q → GroupTheory.invDistr (Ring→Group ℤ/2[X,Y]R) x y
+                  ∙ addComm _ _
+                  ∙ cong₂ _add_ p q
+
+  +Trivℤ/2[X,Y] : (x : fst ℤ/2[X,Y]) → x add x ≡ neutral
+  +Trivℤ/2[X,Y] x = cong (x add_ ) (sym (-≡id-ℤ/2[X,Y] x))
+                   ∙ +InvR (snd ℤ/2[X,Y]R) x
+
+  -ConstH* : ∀ {ℓ} {A : Type ℓ} → (x : fst (H*R ℤ/2Ring A))
+    → -_ (snd (H*R ℤ/2Ring A)) x ≡ x
+  -ConstH* {A = A} = DS-Ind-Prop.f _ _ _ _
+    (λ _ → trunc _ _)
+    refl
+    (λ r a → cong (base r) (-ₕConst-ℤ/2 r a))
+    λ {x} {y} ind1 ind2 → RingTheory.-Dist (H*R ℤ/2Ring A) x y
+                        ∙ cong₂ _add_ ind1 ind2
+
+  +TrivH* : ∀ {ℓ} {A : Type ℓ}
+    → (x : fst (H*R ℤ/2Ring A)) → x add x ≡ neutral
+  +TrivH* {A = A} x = cong (x add_) (sym (-ConstH* x))
+               ∙ +InvR (snd (H*R ℤ/2Ring A)) x
+
+-- Construction of the equivalent polynomial ring
+<X³,Y²,XY+X²> : FinVec (fst ℤ/2[X,Y]) 3
+<X³,Y²,XY+X²> zero = base (3 ∷ (0 ∷ [])) 1
+<X³,Y²,XY+X²> one = base (0 ∷ (2 ∷ [])) 1
+<X³,Y²,XY+X²> two = base (1 ∷ (1 ∷ [])) 1 add base (2 ∷ (0 ∷ [])) 1
+
+ℤ/2[X,Y]/<X³,Y²,XY+X²> : CommRing ℓ-zero
+ℤ/2[X,Y]/<X³,Y²,XY+X²> = PolyCommRing-Quotient ℤ/2CommRing <X³,Y²,XY+X²>
+
+private
+  _·Z/_ = _·r_ (snd (CommRing→Ring ℤ/2[X,Y]/<X³,Y²,XY+X²>))
+
+  makeHomℤ[X,Y] : ∀ {ℓ'} {R : Ring ℓ'} (f : fst ℤ/2[X,Y] → fst R)
+    → IsRingHom (snd (CommRing→Ring ℤ/2[X,Y])) f (snd R)
+    → f (base (3 ∷ (0 ∷ [])) 1) ≡ 0r (snd R)
+    → f (base (0 ∷ (2 ∷ [])) 1) ≡ 0r (snd R)
+    → f ((base (1 ∷ (1 ∷ [])) 1) add (base (2 ∷ (0 ∷ [])) 1)) ≡ 0r (snd R)
+    → RingHom (CommRing→Ring ℤ/2[X,Y]/<X³,Y²,XY+X²>) R
+  makeHomℤ[X,Y] {R = R} f ishom id1 id2 id3 = (λ x → fst k x)
+    , makeIsRingHom (IsRingHom.pres1 (snd k))
+                    (λ x y → IsRingHom.pres+ (snd k) x y)
+                    λ x y → IsRingHom.pres· (snd k) x y
+    where
+    -- verbose definition (speeds up type checking a bit)
+    k = Quotient-FGideal-CommRing-Ring.inducedHom
+      ℤ/2[X,Y]
+      R
+      (f , ishom)
+      <X³,Y²,XY+X²>
+      λ { zero → id1 ; one → id2 ; two → id3}
+
+-- Inclusion of basics
+
+HⁿKlein→ℤ/2[X,Y]/I : (n : ℕ)
+  → coHom n ℤ/2 KleinBottle → fst ℤ/2[X,Y]/<X³,Y²,XY+X²>
+HⁿKlein→ℤ/2[X,Y]/I zero a =
+  [ base (0 ∷ 0 ∷ []) (H⁰[K²,ℤ/2]≅ℤ/2 .fst .fst a) ]
+HⁿKlein→ℤ/2[X,Y]/I one a =
+    [ base (1 ∷ 0 ∷ [])  (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst .fst a .fst)
+  add base (0 ∷ 1 ∷ [])  (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst .fst a .snd) ]
+HⁿKlein→ℤ/2[X,Y]/I two a =
+  [ base (2 ∷ 0 ∷ []) (H²[K²,ℤ/2]≅ℤ/2* .fst .fst a) ]
+HⁿKlein→ℤ/2[X,Y]/I (suc (suc (suc n))) _ = [ neutral ]
+
+-- xⁿ ↦ ... : Hⁿ(K²,ℤ/2)
+incL : (x : ℕ) → coHom x ℤ/2 KleinBottle
+incL zero = 1ₕ {G'' = ℤ/2Ring}
+incL one = K²gen.α
+incL two = α⌣α
+incL (suc (suc (suc n))) = 0ₕ _
+
+-- yⁿ ↦ ... : Hⁿ(K²,ℤ/2)
+incR : (x : ℕ) → coHom x ℤ/2 KleinBottle
+incR zero = 1ₕ {G'' = ℤ/2Ring}
+incR one = K²gen.β
+incR (suc (suc n)) = 0ₕ _
+
+-- Map ℤ/2[X,Y] → H*(K²,ℤ/2)
+ℤ/2[X,Y]→H*Klein-fun : fst ℤ/2[X,Y] → fst (H*R ℤ/2Ring KleinBottle)
+ℤ/2[X,Y]→H*Klein-fun = DS-Rec-Set.f _ _ _ _
+  trunc neutral
+  (λ x y → mainFun y x)
+  _add_ addAssoc addRid addComm
+  (λ _ → refl)
+  λ r a b → lem a b r
+  where
+  mainFun : Cubical.Data.Fin.Fin 2
+     → (r : Vec ℕ 2)
+     → fst (H*R ℤ/2Ring KleinBottle)
+  mainFun =
+    ℤ/2-rec (λ _ → neutral)
+             λ {(x ∷ y ∷ []) → base (x +' y) (incL x ⌣ incR y)}
+
+  lem : (a b : Cubical.Data.Fin.Fin 2) (r : Vec ℕ 2)
+    → (mainFun a r add mainFun b r)
+     ≡ mainFun ((snd (CommRing→Ring ℤ/2CommRing) +r a) b) r
+  lem =
+    ℤ/2-elim
+     (ℤ/2-elim
+     (λ r → addRid _)
+      λ r → +IdL (snd (H*R ℤ/2Ring KleinBottle)) (mainFun 1 r))
+     (ℤ/2-elim
+     (λ r → +IdR (snd (H*R ℤ/2Ring KleinBottle)) (mainFun 1 r))
+      λ r → +TrivH* (mainFun 1 r))
+
+-- Homomorphism proof
+isHomℤ/2[X,Y]→H*Klein :
+  IsRingHom (snd ℤ/2[X,Y]R)
+            ℤ/2[X,Y]→H*Klein-fun
+            (snd (H*R ℤ/2Ring KleinBottle))
+isHomℤ/2[X,Y]→H*Klein = makeIsRingHom refl (λ _ _ → refl)
+  (DS-Ind-Prop.f _ _ _ _
+    (λ _ → isPropΠ λ _ → trunc _ _)
+    (λ y → cong ℤ/2[X,Y]→H*Klein-fun
+             (RingTheory.0LeftAnnihilates ℤ/2[X,Y]R y)
+           ∙ sym (RingTheory.0LeftAnnihilates (H*R ℤ/2Ring KleinBottle)
+              (ℤ/2[X,Y]→H*Klein-fun y)))
+    (λ r a
+      → DS-Ind-Prop.f _ _ _ _
+          (λ _ → trunc _ _)
+          (cong ℤ/2[X,Y]→H*Klein-fun
+            (RingTheory.0RightAnnihilates (ℤ/2[X,Y]R) (base r a))
+          ∙ sym (RingTheory.0RightAnnihilates (H*R ℤ/2Ring KleinBottle) _))
+       (λ r2 a2 → lem a a2 r r2)
+         λ ind ind2
+           → cong₂ (_+r_ (snd (H*R ℤ/2Ring KleinBottle))) ind ind2
+                  ∙ sym (·DistR+ (snd (H*R ℤ/2Ring KleinBottle)) _ _ _))
+    λ ind ind2 y
+      → cong₂ (_+r_ (snd (H*R ℤ/2Ring KleinBottle))) (ind y) (ind2 y))
+  where
+  lem : (a b : fst ℤ/2) (r s : Vec ℕ 2)
+    → ℤ/2[X,Y]→H*Klein-fun (base r a ·Z/2 base s b)
+    ≡ (ℤ/2[X,Y]→H*Klein-fun (base r a) ⌣' ℤ/2[X,Y]→H*Klein-fun (base s b))
+  lem =
+    ℤ/2-elim
+    (ℤ/2-elim
+     (λ r s
+       → cong ℤ/2[X,Y]→H*Klein-fun (base-neutral _)
+        ∙ cong₂ _⌣'_
+           (cong ℤ/2[X,Y]→H*Klein-fun (sym (base-neutral r)))
+           (cong ℤ/2[X,Y]→H*Klein-fun (sym (base-neutral s))))
+     λ r s
+       → cong ℤ/2[X,Y]→H*Klein-fun
+                (cong (_·Z/2 (base s 1)) (base-neutral _))
+            ∙ cong (_⌣' ℤ/2[X,Y]→H*Klein-fun (base s 1))
+              (cong ℤ/2[X,Y]→H*Klein-fun (sym (base-neutral r))))
+    (ℤ/2-elim
+     (λ r s → cong ℤ/2[X,Y]→H*Klein-fun
+                (cong (base r 1 ·Z/2_) (base-neutral s))
+             ∙ sym (RingTheory.0RightAnnihilates
+                   (H*R ℤ/2Ring KleinBottle)
+                   (ℤ/2[X,Y]→H*Klein-fun (base r 1)))
+             ∙ cong (ℤ/2[X,Y]→H*Klein-fun (base r 1) ⌣'_)
+                    (cong ℤ/2[X,Y]→H*Klein-fun (sym (base-neutral s))))
+     1-1-case)
+     where
+     PathP-lem : (n m : ℕ) (p : n ≡ m)
+       (x : coHom n ℤ/2 KleinBottle) (y : coHom m ℤ/2 KleinBottle)
+       → PathP (λ i → coHom (p i) ℤ/2 KleinBottle) x y
+       → Path (H*R ℤ/2Ring KleinBottle .fst) (base n x) (base m y)
+     PathP-lem n = J> λ x → J> refl
+
+     incR-pres⌣ : (n m : ℕ)
+               → incR (n +' m) ≡ (_⌣_ {G'' = ℤ/2Ring} (incR n) (incR m))
+     incR-pres⌣ zero m = sym (1ₕ-⌣ m (incR m))
+     incR-pres⌣ one zero =
+       sym (transportRefl (incR 1)) ∙ sym (⌣-1ₕ 1 (incR one))
+     incR-pres⌣ one one =
+          sym (IsGroupHom.pres1 (snd (invGroupEquiv H²[K²,ℤ/2]≅ℤ/2)))
+       ∙∙ sym (cong (ℤ/2→H²K²) β²↦0)
+       ∙∙ H²K²→ℤ/2→H²K² (_⌣_ {G'' = ℤ/2Ring} K²gen.β K²gen.β)
+     incR-pres⌣ one (suc (suc m)) =
+       isContr→isProp (isContr-HⁿKleinBottle m ℤ/2) _ _
+     incR-pres⌣ (suc (suc n)) zero =
+         sym (transportRefl (incR (2 + n)))
+       ∙ sym (⌣-1ₕ (suc (suc n)) (incR (suc (suc n))))
+     incR-pres⌣ (suc (suc n)) (suc m) =
+       sym (0ₕ-⌣ (suc (suc n)) (suc m) (incR (suc m)))
+
+     incL-pres⌣ : (n m : ℕ)
+       → incL (n +' m) ≡ _⌣_ {G'' = ℤ/2Ring} (incL n) (incL m)
+     incL-pres⌣ zero m = sym (1ₕ-⌣ m (incL m))
+     incL-pres⌣ one zero =
+       sym (transportRefl (incL 1)) ∙ sym (⌣-1ₕ 1 (incL one))
+     incL-pres⌣ one one = refl
+     incL-pres⌣ one (suc (suc m)) =
+       isContr→isProp (isContr-HⁿKleinBottle m ℤ/2) _ _
+     incL-pres⌣ two zero =
+       sym (transportRefl (incL 2)) ∙ sym (⌣-1ₕ 2 (incL 2))
+     incL-pres⌣ two (suc m) =
+       isContr→isProp (isContr-HⁿKleinBottle m ℤ/2) _ _
+     incL-pres⌣ (suc (suc (suc n))) m =
+       isContr→isProp (subst (λ n → isContr (coHom n ℤ/2 KleinBottle))
+          (sym (+'≡+ (3 + n) m))
+          (isContr-HⁿKleinBottle (n + m) ℤ/2)) _ _
+
+     1-1-case : (r s : Vec ℕ 2)
+      → ℤ/2[X,Y]→H*Klein-fun (base r 1 ·Z/2 base s 1)
+       ≡ (ℤ/2[X,Y]→H*Klein-fun (base r 1)
+      ⌣'  ℤ/2[X,Y]→H*Klein-fun (base s 1))
+     1-1-case (x ∷ y ∷ []) (x2 ∷ y2 ∷ []) =
+        (λ i → base ((+'≡+ x x2 (~ i)) +' (+'≡+ y y2 (~ i)))
+             (incL (+'≡+ x x2 (~ i)) ⌣ incR (+'≡+ y y2 (~ i))))
+       ∙ cong (base ((x +' x2) +' (y +' y2)))
+              (cong₂ _⌣_ (incL-pres⌣ x x2) (incR-pres⌣ y y2))
+       ∙ PathP-lem _ _ (sym (+'-assoc x x2 (y +' y2))) _ _
+           (assoc⌣Dep x x2 (y +' y2) (incL x) (incL x2) (incR y ⌣ incR y2))
+       ∙ PathP-lem _ _ (cong (x +'_) (+'-assoc x2 y y2)) _ _
+             (λ i → _⌣_ {G'' = ℤ/2Ring} (incL x)
+              (assoc⌣Dep x2 y y2 (incL x2) (incR y) (incR y2) (~ i)))
+       ∙ PathP-lem _ _ (λ i → x +' ((+'-comm x2 y i) +' y2)) _ _
+          (λ i → _⌣_ {G'' = ℤ/2Ring} (incL x)
+                 (_⌣_ {G'' = ℤ/2Ring}
+                  (⌣-comm-Klein x2 y (incL x2) (incR y) i) (incR y2)))
+       ∙ PathP-lem _ _ (cong (x +'_) (sym (+'-assoc y x2 y2))) _ _
+          (λ i → _⌣_ {G'' = ℤ/2Ring} (incL x)
+           (assoc⌣Dep y x2 y2 (incR y) (incL x2) (incR y2) i))
+       ∙ PathP-lem _ _ (+'-assoc x y (x2 +' y2)) _ _
+          (λ i → assoc⌣Dep x y (x2 +' y2) (incL x) (incR y)
+            (_⌣_ {G'' = ℤ/2Ring} (incL x2) (incR y2)) (~ i))
+
+-- Induced map ℤ/2[X,Y]/I → H*(K²,ℤ/2)
+ℤ/2[X,Y]/I→H*Klein :
+  RingHom (CommRing→Ring ℤ/2[X,Y]/<X³,Y²,XY+X²>)
+          (H*R ℤ/2Ring KleinBottle)
+ℤ/2[X,Y]/I→H*Klein =
+  makeHomℤ[X,Y]
+    ℤ/2[X,Y]→H*Klein-fun
+    isHomℤ/2[X,Y]→H*Klein
+    (base-neutral _) (base-neutral _)
+    (IsRingHom.pres+ isHomℤ/2[X,Y]→H*Klein
+      (base (1 ∷ (1 ∷ [])) 1) (base (2 ∷ (0 ∷ [])) 1)
+    ∙ base-add 2 _ _
+    ∙ cong (base 2)
+       (cong₂ (_+ₕ_) αβ≡
+             (⌣-1ₕ 2 (incL 2) ∙ transportRefl (incL 2))
+       ∙ +ₕ≡id-ℤ/2 2 (_⌣_ {G'' = ℤ/2Ring} K²gen.α K²gen.α))
+    ∙ base-neutral 2)
+  where
+  αβ≡ : α⌣β ≡ α⌣α
+  αβ≡ = sym (H²K²→ℤ/2→H²K² (_⌣_ {G'' = ℤ/2Ring} K²gen.α K²gen.β))
+     ∙∙ cong ℤ/2→H²K² (αβ↦1 ∙ sym α²↦1)
+     ∙∙ H²K²→ℤ/2→H²K² (_⌣_ {G'' = ℤ/2Ring} K²gen.α K²gen.α)
+
+-- Map H*(K²) → ℤ/2[X,Y]/I
+H*Klein→ℤ/2[X,Y]/I :
+    fst (H*R ℤ/2Ring KleinBottle)
+ → fst (CommRing→Ring ℤ/2[X,Y]/<X³,Y²,XY+X²>)
+H*Klein→ℤ/2[X,Y]/I =
+  DS-Rec-Set.f _ _ _ _ squash/ [ neutral ]
+    HⁿKlein→ℤ/2[X,Y]/I _
+    (+Assoc (snd (CommRing→Ring ℤ/2[X,Y]/<X³,Y²,XY+X²>)))
+    (+IdR (snd (CommRing→Ring ℤ/2[X,Y]/<X³,Y²,XY+X²>)))
+    (+Comm (snd (CommRing→Ring ℤ/2[X,Y]/<X³,Y²,XY+X²>)))
+    (λ { zero → cong [_] (base-neutral _)
+      ; one → cong [_] (cong₂ _add_ (base-neutral _) (base-neutral _)
+                      ∙ addRid neutral)
+      ; two → cong [_] (cong (base (2 ∷ 0 ∷ []))
+                        (IsGroupHom.pres1 (snd (H²[K²,ℤ/2]≅ℤ/2*)))
+                      ∙ base-neutral _)
+      ; (suc (suc (suc r))) → refl})
+    λ { zero a b → cong [_] (base-add _ _ _ ∙ cong (base (0 ∷ 0 ∷ []))
+                     (sym (IsGroupHom.pres· (snd (H⁰[K²,ℤ/2]≅ℤ/2)) a b)))
+      ; one a b → cong [_] (move4 _ _ _ _ _add_ addAssoc addComm
+      ∙ cong₂ _add_ (base-add _ _ _ ∙ cong (base (1 ∷ 0 ∷ []))
+                    (cong fst (sym
+                     (IsGroupHom.pres· (snd (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2)) a b))))
+                    (base-add _ _ _ ∙ cong (base (0 ∷ 1 ∷ []))
+                    (cong snd
+                     (sym (IsGroupHom.pres· (snd (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2)) a b)))))
+      ; two a b → cong [_] (base-add _ _ _ ∙ cong (base (2 ∷ 0 ∷ []))
+                   (sym (IsGroupHom.pres· (snd (H²[K²,ℤ/2]≅ℤ/2*)) a b)))
+      ; (suc (suc (suc n))) → λ a b → cong [_] (addRid neutral)}
+
+-- The equivalence
+ℤ/2[X,Y]/<X³,Y²,XY+X²>≅H*KleinBottle :
+  RingEquiv (CommRing→Ring ℤ/2[X,Y]/<X³,Y²,XY+X²>)
+            (H*R ℤ/2Ring KleinBottle)
+fst ℤ/2[X,Y]/<X³,Y²,XY+X²>≅H*KleinBottle = isoToEquiv is
+  where
+  is : Iso  _ _
+  fun is = ℤ/2[X,Y]/I→H*Klein .fst
+  inv is = H*Klein→ℤ/2[X,Y]/I
+  rightInv is = DS-Ind-Prop.f _ _ _ _
+    (λ _ → trunc _ _)
+    refl
+    (λ { zero a → lem₀ a _ refl
+       ; one a → lem₁ a _ _ refl
+       ; two a → lem₂ a  _ refl
+       ; (suc (suc (suc r))) a →
+           sym (base-neutral _)
+         ∙ cong (base (3 + r))
+            (isContr→isProp (isContr-HⁿKleinBottle r ℤ/2)
+             (0ₕ (3 + r)) a)})
+    λ {x} {y} ind1 ind2
+      → IsRingHom.pres+ (ℤ/2[X,Y]/I→H*Klein .snd)
+          (H*Klein→ℤ/2[X,Y]/I x) (H*Klein→ℤ/2[X,Y]/I y)
+         ∙ cong₂ _add_ ind1 ind2
+    where
+    lem₀ : (a : _) (x : _)
+      → H⁰[K²,ℤ/2]≅ℤ/2 .fst .fst a ≡ x
+      → ℤ/2[X,Y]/I→H*Klein .fst (H*Klein→ℤ/2[X,Y]/I (base zero a))
+       ≡ base zero a
+    lem₀ a =
+      ℤ/2-elim
+       (λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ H*Klein→ℤ/2[X,Y]/I) (help id)
+              ∙ sym (help id))
+      λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst)
+               (cong [_] (cong (base (0 ∷ 0 ∷ [])) id))
+            ∙ cong (base zero)
+              (sym (cong (invEq (H⁰[K²,ℤ/2]≅ℤ/2 .fst)) id)
+             ∙ retEq (fst H⁰[K²,ℤ/2]≅ℤ/2) a)
+      where
+      help : H⁰[K²,ℤ/2]≅ℤ/2 .fst .fst a ≡ 0
+        → Path (fst (H*R ℤ/2Ring KleinBottle)) (base zero a) neutral
+      help id' =
+        sym (cong (base zero)
+            (sym (cong (invEq (H⁰[K²,ℤ/2]≅ℤ/2 .fst)) id'
+           ∙ IsGroupHom.pres1 (isGroupHomInv (H⁰[K²,ℤ/2]≅ℤ/2)))
+           ∙ retEq (fst H⁰[K²,ℤ/2]≅ℤ/2) a))
+        ∙ base-neutral zero
+
+    lem₁ : (a : _) → (x y : _)
+      → H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst .fst a ≡ (x , y)
+      → ℤ/2[X,Y]/I→H*Klein .fst (H*Klein→ℤ/2[X,Y]/I (base one a))
+       ≡ base one a
+    lem₁ a =
+      ℤ/2-elim
+        (ℤ/2-elim
+          (λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ [_])
+            (cong₂ _add_ (cong (base (1 ∷ 0 ∷ []))
+              (cong fst id))
+              (cong (base (0 ∷ 1 ∷ []))
+              (cong snd id)))
+              ∙ addRid neutral
+              ∙ sym (help a id))
+          λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ [_])
+                   (cong₂ _add_
+                     (cong (base (1 ∷ 0 ∷ [])) (cong fst id)
+                     ∙ base-neutral _)
+                     (cong (base (0 ∷ 1 ∷ [])) (cong snd id))
+                   ∙ addComm _ _ ∙ addRid _)
+               ∙∙ cong (base 1) (1ₕ-⌣ 1 K²gen.β)
+               ∙∙ cong (base 1) (sym (retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) K²gen.β)
+                     ∙∙ cong (invEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst)) (sym id)
+                     ∙∙ retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) a))
+        (ℤ/2-elim
+          (λ id → (cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ [_])
+                   (cong₂ _add_
+                     (cong (base (1 ∷ 0 ∷ [])) (cong fst id))
+                     (cong (base (0 ∷ 1 ∷ [])) (cong snd id) ∙ base-neutral _)
+                   ∙ addRid _)
+                ∙ cong (base 1)
+                   (    (⌣-1ₕ 1 K²gen.α ∙ transportRefl K²gen.α)
+                      ∙ (sym (retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) K²gen.α)
+                     ∙∙ cong (invEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst)) (α↦1 ∙ sym id)
+                     ∙∙ retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) a))))
+          λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ [_])
+                   (cong₂ _add_
+                     (cong (base (1 ∷ 0 ∷ [])) (cong fst id))
+                     (cong (base (0 ∷ 1 ∷ [])) (cong snd id)))
+                ∙ IsRingHom.pres+ (snd ℤ/2[X,Y]/I→H*Klein)
+                   [ base (1 ∷ 0 ∷ []) 1 ] [ base (0 ∷ 1 ∷ []) 1 ]
+                ∙ cong₂ _add_
+                        (cong (base one) (⌣-1ₕ 1 (incL 1) ∙ transportRefl K²gen.α))
+                        (cong (base one) (1ₕ-⌣ 1 (incR 1)))
+                ∙ base-add 1 K²gen.α K²gen.β
+                ∙ cong (base one)
+                   (sym (retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) (K²gen.α +ₕ K²gen.β))
+                 ∙∙ (cong (invEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst)) (sym id))
+                 ∙∙ retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) a))
+      where
+      help : (a : _) → H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst .fst a ≡ (0 , 0)
+        → Path (fst (H*R ℤ/2Ring KleinBottle)) (base one a) neutral
+      help a p =
+         (sym (cong (base one)
+                  (sym (cong (invEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst)) p
+                 ∙ IsGroupHom.pres1 (isGroupHomInv (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2)))
+                 ∙ retEq (H¹[K²,ℤ/2]≅ℤ/2×ℤ/2 .fst) a)))
+        ∙ base-neutral one
+
+    lem₂ : (a : _) (x : _) → H²[K²,ℤ/2]≅ℤ/2* .fst .fst a ≡ x
+      → ℤ/2[X,Y]/I→H*Klein .fst (H*Klein→ℤ/2[X,Y]/I (base two a))
+       ≡ base two a
+    lem₂ a =
+      ℤ/2-elim
+       (λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst ∘ H*Klein→ℤ/2[X,Y]/I)
+                  (cong (base 2) (help1 id) ∙ base-neutral _)
+              ∙∙ sym (base-neutral _)
+              ∙∙ cong (base 2) (sym (help1 id)))
+        λ id → cong (ℤ/2[X,Y]/I→H*Klein .fst)
+                 (cong [_] (cong (base (2 ∷ 0 ∷ []))
+                     (cong (H²[K²,ℤ/2]≅ℤ/2* .fst .fst) (help2 id)
+                     ∙ α²↦1') ))
+             ∙∙ cong (base 2) (⌣-1ₕ 2 (incL 2) ∙ transportRefl (incL 2))
+             ∙∙ cong (base two) (sym (help2 id))
+      where
+      help1 : H²[K²,ℤ/2]≅ℤ/2* .fst .fst a ≡ 0 → a ≡ 0ₕ 2
+      help1 p = sym (retEq (H²[K²,ℤ/2]≅ℤ/2* .fst) a)
+           ∙ cong (invEq (H²[K²,ℤ/2]≅ℤ/2* .fst)) p
+           ∙ IsGroupHom.pres1 (isGroupHomInv H²[K²,ℤ/2]≅ℤ/2*)
+
+      help2 : H²[K²,ℤ/2]≅ℤ/2* .fst .fst a ≡ 1 → a ≡ α⌣α
+      help2 p = sym (retEq (H²[K²,ℤ/2]≅ℤ/2* .fst) a)
+          ∙∙ cong (invEq (H²[K²,ℤ/2]≅ℤ/2* .fst)) (p ∙ sym α²↦1')
+          ∙∙ retEq (H²[K²,ℤ/2]≅ℤ/2* .fst) α⌣α
+
+  leftInv is =
+    SQ.elimProp
+      (λ _ → squash/ _ _)
+      (DS-Ind-Prop.f _ _ _ _
+        (λ _ → squash/ _ _)
+        refl
+        (λ r a → main a r)
+        λ {x} {y} ind1 ind2
+          → cong₂ (_+r_ (snd (CommRing→Ring ℤ/2[X,Y]/<X³,Y²,XY+X²>)))
+                   ind1 ind2)
+    where
+    clem : (x y : ℕ)
+      → H*Klein→ℤ/2[X,Y]/I
+          (ℤ/2[X,Y]/I→H*Klein .fst
+            [ base (suc (suc (suc x)) ∷ y ∷ []) 1 ])
+      ≡ [ neutral ]
+    clem x zero = refl
+    clem x (suc n) = refl
+
+    help : (y : ℕ) →
+      Path (fst (CommRing→Ring ℤ/2[X,Y]/<X³,Y²,XY+X²>))
+           [ base (one ∷ suc (suc y) ∷ []) 1 ]
+           [ neutral ]
+    help y = eq/ _ _
+      ∣ (λ { zero → neutral
+          ; one → base (1 ∷ y ∷ []) 1
+          ; two → neutral})
+      , (sym (addRid _)
+       ∙ addComm (base (1 ∷ suc (suc y) ∷ []) 1 add neutral) neutral)
+      ∙ (λ i → neutral add (base (1 ∷ (+-comm 2 y i) ∷ []) 1
+                        add (addRid neutral (~ i)))) ∣₁
+
+    help2 : (y : ℕ)
+      → ℤ/2[X,Y]/I→H*Klein .fst [ base (zero ∷ suc (suc y) ∷ []) 1 ]
+       ≡ neutral
+    help2 zero = cong (base 2) (1ₕ-⌣ 2 (incR two))
+            ∙ base-neutral _
+    help2 (suc y) = base-neutral _
+
+    help3 : (x y : ℕ)
+      → ℤ/2[X,Y]/I→H*Klein .fst [ base (x ∷ suc (suc y) ∷ []) 1 ]
+       ≡ neutral
+    help3 zero y = help2 y
+    help3 (suc x) y =
+         (λ i → base (suc (suc (+-suc x y i)))
+                 (transp (λ j → coHom (suc (suc (+-suc x y (i ∧ j))))
+                   ℤ/2 KleinBottle) (~ i)
+                  (_⌣_ {G'' = ℤ/2Ring} (incL (suc x)) (incR (suc (suc y))))))
+       ∙ cong (base (suc (suc (suc (x + y)))))
+          (isContr→isProp (isContr-HⁿKleinBottle (x + y) ℤ/2) _ _)
+       ∙ base-neutral _
+
+    main-1 : (r : _)
+      → H*Klein→ℤ/2[X,Y]/I (ℤ/2[X,Y]/I→H*Klein .fst [ base r 1 ])
+      ≡ [ base r 1 ]
+    main-1 (zero ∷ zero ∷ []) = refl
+    main-1 (zero ∷ one ∷ []) =
+      cong (H*Klein→ℤ/2[X,Y]/I)
+           (cong (base 1) (1ₕ-⌣ 1 (incR 1)))
+        ∙ cong [_] (cong₂ _add_ (base-neutral _)
+                   (λ _ → base (0 ∷ 1 ∷ []) 1)
+                 ∙ addComm _ _ ∙ addRid _)
+    main-1 (zero ∷ suc (suc y) ∷ []) =
+      cong H*Klein→ℤ/2[X,Y]/I (help2 y)
+     ∙ eq/ _ _
+       ∣ (λ {zero → neutral
+           ; one → base (0 ∷ (y ∷ [])) 1
+           ; two → neutral})
+      , cong (neutral add_)
+         (((λ i → base (0 ∷ (+-comm 2 y i) ∷ []) 1)
+        ∙ sym (addRid (base (0 ∷ (y + 2) ∷ []) 1)))
+       ∙ cong (base (0 ∷ (y + 2) ∷ []) 1 add_) (sym (addRid _))) ∣₁
+    main-1 (one ∷ zero ∷ []) =
+      cong H*Klein→ℤ/2[X,Y]/I
+        (cong (base 1) (⌣-1ₕ 1 (incL one) ∙ transportRefl _))
+       ∙ cong [_] (cong₂ _add_ (cong (base (1 ∷ 0 ∷ []))
+                                (cong fst α↦1))
+                               (base-neutral _)
+                 ∙ addRid _)
+    main-1 (one ∷ one ∷ []) =
+      cong [_] (cong (base (2 ∷ 0 ∷ [])) αβ↦1')
+       ∙ eq/ _ _ ∣ (λ {zero → neutral
+                     ; one → neutral
+                     ; two → base (0 ∷ 0 ∷ []) 1})
+               , ((addComm _ _
+                ∙ sym (addRid _)
+                ∙ addComm (base (1 ∷ 1 ∷ []) 1
+                      add (base (2 ∷ 0 ∷ []) 1))
+                      neutral
+                ∙ sym (addRid _)
+                ∙ addComm (neutral add (base (1 ∷ 1 ∷ []) 1
+                      add (base (2 ∷ 0 ∷ []) 1))) neutral)
+                ∙ λ i → neutral add
+                  (neutral add (addRid
+                   (base (1 ∷ 1 ∷ []) 1
+                    add (base (2 ∷ 0 ∷ []) 1)) (~ i)))) ∣₁
+    main-1 (one ∷ suc (suc y) ∷ []) =
+      cong H*Klein→ℤ/2[X,Y]/I (help3 one y) ∙ sym (help y)
+    main-1 (two ∷ zero ∷ []) =
+      cong [_] (cong (base (2 ∷ 0 ∷ []))
+        (cong (H²[K²,ℤ/2]≅ℤ/2* .fst .fst)
+        (⌣-1ₕ 2 (incL 2) ∙ transportRefl _)
+      ∙ α²↦1'))
+    main-1 (two ∷ suc y ∷ []) =
+      eq/ neutral _
+       ∣ (λ {zero → base (0 ∷ y ∷ []) 1
+           ; one → neutral
+           ; two → base (1 ∷ y ∷ []) 1})
+       , ((addComm _ _ ∙ addRid _
+       ∙ ((((λ i → base (2 ∷ +-comm 1 y i ∷ []) 1)
+         ∙ sym (addRid _))
+         ∙ cong (base (2 ∷ y + 1 ∷ []) (fsuc fzero) add_)
+            (sym (base-neutral _)
+            ∙ sym (base-add (3 ∷ y + 0 ∷ []) 1 1)))
+       ∙ addComm _ _)
+       ∙ sym (addAssoc _ _ _))
+       ∙∙ cong (base (3 ∷ y + 0 ∷ []) (fsuc fzero) add_)
+          (addComm _ _
+          ∙ sym (addComm _ _ ∙ addRid _))
+       ∙∙ (λ i → base (3 ∷ (y + 0) ∷ []) 1
+            add (neutral
+            add addRid (base (2 ∷ (y + 1) ∷ []) 1
+            add base (3 ∷ (y + 0) ∷ []) 1 ) (~ i)))) ∣₁
+    main-1 (suc (suc (suc x)) ∷ y ∷ []) =
+      clem x y
+      ∙ eq/ neutral _
+        ∣ (λ {zero → base (x ∷ y ∷ []) 1
+           ; one → neutral
+           ; two → neutral})
+        , ((addComm neutral (base ((3 + x) ∷ y ∷ []) 1)
+        ∙ cong (base ((3 + x) ∷ y ∷ []) 1 add_) (sym (addRid neutral)))
+         ∙ λ i → base ((+-comm 3 x i) ∷ (+-comm 0 y i) ∷ []) 1
+                  add (neutral add (addRid neutral (~ i)))) ∣₁
+
+    main : (a : ℤ/2 .fst) (r : _)
+      → H*Klein→ℤ/2[X,Y]/I (ℤ/2[X,Y]/I→H*Klein .fst [ base r a ]) ≡ [ base r a ]
+    main = ℤ/2-elim (λ r → cong (H*Klein→ℤ/2[X,Y]/I ∘ ℤ/2[X,Y]/I→H*Klein .fst)
+                             (cong [_] (base-neutral r))
+                          ∙ cong [_] (sym (base-neutral r)))
+                     main-1
+snd ℤ/2[X,Y]/<X³,Y²,XY+X²>≅H*KleinBottle = ℤ/2[X,Y]/I→H*Klein .snd
+
+H*KleinBottle≅ℤ/2[X,Y]/<X³,Y²,XY+X²> :
+  RingEquiv (H*R ℤ/2Ring KleinBottle)
+            (CommRing→Ring ℤ/2[X,Y]/<X³,Y²,XY+X²>)
+H*KleinBottle≅ℤ/2[X,Y]/<X³,Y²,XY+X²> =
+  RingEquivs.invRingEquiv ℤ/2[X,Y]/<X³,Y²,XY+X²>≅H*KleinBottle
diff --git a/Cubical/Homotopy/EilenbergMacLane/GroupStructure.agda b/Cubical/Homotopy/EilenbergMacLane/GroupStructure.agda
index 0ae2caf17..d48839b8f 100644
--- a/Cubical/Homotopy/EilenbergMacLane/GroupStructure.agda
+++ b/Cubical/Homotopy/EilenbergMacLane/GroupStructure.agda
@@ -413,3 +413,8 @@ module _ {G : AbGroup ℓ} where
     sym (assocₖ n y x (-[ n ]ₖ x))
     ∙∙ cong (λ x → y +[ n ]ₖ x) (rCancelₖ n x)
     ∙∙ rUnitₖ n y
+
+-0ₖ : ∀ {ℓ} {G : AbGroup ℓ} (n : ℕ) → -[ n ]ₖ (0ₖ {G = G} n) ≡ 0ₖ n
+-0ₖ {G = G} zero = GroupTheory.inv1g (AbGroup→Group G)
+-0ₖ (suc zero) = refl
+-0ₖ (suc (suc n)) = refl
diff --git a/Cubical/Homotopy/EilenbergMacLane/Order2.agda b/Cubical/Homotopy/EilenbergMacLane/Order2.agda
index 3abe5ba16..64d569ffe 100644
--- a/Cubical/Homotopy/EilenbergMacLane/Order2.agda
+++ b/Cubical/Homotopy/EilenbergMacLane/Order2.agda
@@ -215,3 +215,7 @@ symConst-ℤ/2 = EMZ/2.symConstEM
 
 symConst-ℤ/2-refl : {n : ℕ} → symConst-ℤ/2 n (0ₖ n) refl ≡ refl
 symConst-ℤ/2-refl = EMZ/2.symConstEM-refl
+
++ₖ≡id-ℤ/2 : (n : ℕ) (x : EM ℤ/2 n) → x +ₖ x ≡ 0ₖ n
++ₖ≡id-ℤ/2 zero = ℤ/2-elim refl refl
++ₖ≡id-ℤ/2 (suc n) x = cong (x +ₖ_) (sym (-ₖConst-ℤ/2 n x)) ∙ rCancelₖ (suc n) x