{-# OPTIONS --safe --lossy-unification #-}

module Cubical.Cohomology.EilenbergMacLane.Groups.RP2 where

open import Cubical.Cohomology.EilenbergMacLane.Base
open import Cubical.Cohomology.EilenbergMacLane.Groups.Connected

open import Cubical.Homotopy.EilenbergMacLane.GroupStructure
open import Cubical.Homotopy.EilenbergMacLane.Order2
open import Cubical.Homotopy.EilenbergMacLane.Properties
open import Cubical.Homotopy.EilenbergMacLane.Base
open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.Loopspace

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Path
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Nat renaming (_+_ to _+ℕ_)
open import Cubical.Data.Unit
open import Cubical.Data.Sigma
open import Cubical.Data.Fin

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
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.AbGroup
open import Cubical.Algebra.AbGroup.Instances.IntMod
open import Cubical.Algebra.Group.Subgroup
open import Cubical.Algebra.Group.QuotientGroup

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.EilenbergMacLane1 as EM1
open import Cubical.HITs.RPn
open import Cubical.HITs.SetQuotients as SQ

open AbGroupStr

private
  variable
     ℓ' : Level
    A : Type 

module RP²Conn {B : (RP²  A)  Type } where
  elim₁ :
      isConnected 2 A
     ((x : _)  isProp (B x))
     (a* : A)
     ((l1 : a*  a*) (sq : l1  sym l1)
          B (RP²Fun a* l1 sq))
     (x : _)  B x
  elim₁  conA pr a* ind f =
    TR.rec (pr _)
       p  J  a* _  ((l1 : a*  a*) (sq : l1  sym l1)
                         B (RP²Fun a* l1 sq))  B f)
                 ind  subst B (characRP²Fun f) (ind _ _))
                p ind)
      (isConnectedPath 1 conA (f point) a* .fst)

  elim₂ : isConnected 3 A
     ((x : _)  isProp (B x))
     (a* : A)
     ((sq : refl {x = a*}  refl)
          B (RP²Fun a* refl sq))
     (x : _)  B x
  elim₂ conA pr a* ind =
    elim₁ (isConnectedSubtr 2 1 conA)
       _  pr _)
      a*
       l1  TR.rec (isPropΠ  _  pr _))
        (J  l1 _  (sq : l1  sym l1)  B (RP²Fun a* l1 sq))
          ind)
        (isConnectedPath 1
          (isConnectedPath 2 conA a* a*) refl l1 .fst))

  elim₃ : isConnected 4 A
     ((x : _)  isProp (B x))
     (a* : A)
     (B λ _  a*)
     (x : _)  B x
  elim₃ conA pr a* ind =
    elim₂ (isConnectedSubtr 3 1 conA)
      pr
      a*
      λ sq  TR.rec (pr _)
        (J  sq _  B (RP²Fun a* refl sq))
          (subst B (sym (characRP²Fun  _  a*))) ind))
        (isConnectedPath 1
          (isConnectedPath 2
            (isConnectedPath 3 conA _ _) _ _) refl sq .fst)

--- lemmas
Isoℤ/2-morph : {A : Type} (f : A  fst ℤ/2) (0A : A)
   0  fst f 0A  (_+'_ : A  A  A) (-m : A  A)
    x  x)  -m
   (e : IsAbGroup 0A _+'_ -m)
   IsGroupHom (AbGroup→Group (A , abgroupstr 0A _+'_  x  -m x) e) .snd)
                (fst f) ((ℤGroup/ 2) .snd)
Isoℤ/2-morph =
  EquivJ  A f  (0A : A)  0  fst f 0A  (_+'_ : A  A  A) (-m : A  A)
    x  x)  -m
   (e : IsAbGroup 0A _+'_ -m)
   IsGroupHom (AbGroup→Group (A , abgroupstr 0A _+'_  x  -m x) e) .snd)
                (fst f) ((ℤGroup/ 2) .snd))
  (J> λ _+'_  J>
    λ e  makeIsGroupHom (ℤ/2-elim (ℤ/2-elim (IsAbGroup.+IdR e fzero)
      (IsAbGroup.+IdL e 1))
      (ℤ/2-elim (IsAbGroup.+IdR e 1)
        (IsAbGroup.+InvR e 1))))

Iso-Ω²K₂-ℤ/2 : Iso (fst ((Ω^ 2) (EM∙ ℤ/2 2))) (fst ℤ/2)
Iso-Ω²K₂-ℤ/2 =
  compIso (congIso (invIso (Iso-EM-ΩEM+1 {G = ℤ/2} 1)))
    (invIso (Iso-EM-ΩEM+1 {G = ℤ/2} 0))



----- H¹(RP²,ℤ/2) ------
H¹[RP²,ℤ/2]→ℤ/2 : coHom 1 ℤ/2 RP²  fst ℤ/2
H¹[RP²,ℤ/2]→ℤ/2 =
  ST.rec isSetFin
    λ f  ΩEM+1→EM-gen 0 _ (cong f line)

ℤ/2→H¹[RP²,ℤ/2] : fst ℤ/2  coHom 1 ℤ/2 RP²
ℤ/2→H¹[RP²,ℤ/2] x =
    { point  embase
      ; (line i)  emloop x i
      ; (square i j)  symConst-ℤ/2 1 embase (emloop x) i j}) ∣₂

ℤ/2→H¹[RP²,ℤ/2]→ℤ/2 : (x : fst ℤ/2)
   H¹[RP²,ℤ/2]→ℤ/2 (ℤ/2→H¹[RP²,ℤ/2] x)  x
ℤ/2→H¹[RP²,ℤ/2]→ℤ/2 = Iso.leftInv (Iso-EM-ΩEM+1 0)

H¹[RP²,ℤ/2]→ℤ/2→H¹[RP²,ℤ/2]  : (f : coHom 1 ℤ/2 RP²)
   ℤ/2→H¹[RP²,ℤ/2] (H¹[RP²,ℤ/2]→ℤ/2 f)  f
H¹[RP²,ℤ/2]→ℤ/2→H¹[RP²,ℤ/2] =
  ST.elim
     _  isSetPathImplicit)
    (RP²Conn.elim₁ (isConnectedEM 1)
       _  squash₂ _ _)
      embase
      λ l sq  cong ∣_∣₂
        (funExt (elimSetRP²  _  hLevelEM _ 1 _ _)
          refl
          (flipSquare (Iso.rightInv (Iso-EM-ΩEM+1 0) l)))))

H¹[RP²,ℤ/2]≅ℤ/2 : AbGroupEquiv (coHomGr 1 ℤ/2 RP²) ℤ/2
fst H¹[RP²,ℤ/2]≅ℤ/2 = isoToEquiv is
  where
  is : Iso _ _
  Iso.fun is = H¹[RP²,ℤ/2]→ℤ/2
  Iso.inv is = ℤ/2→H¹[RP²,ℤ/2]
  Iso.rightInv is = ℤ/2→H¹[RP²,ℤ/2]→ℤ/2
  Iso.leftInv is = H¹[RP²,ℤ/2]→ℤ/2→H¹[RP²,ℤ/2]
snd H¹[RP²,ℤ/2]≅ℤ/2 =
  isGroupHomInv ((invEquiv (fst H¹[RP²,ℤ/2]≅ℤ/2))
    , makeIsGroupHom λ x y  cong ∣_∣₂
      (funExt (elimSetRP²  _  hLevelEM _ 1 _ _)
                refl
                (flipSquare
                  (emloop-comp _ x y
                   sym (cong₂+₁ (emloop x) (emloop y)))))))

----- H²(RP²,ℤ/2) ------

H²[RP²,ℤ/2]→ℤ/2 : coHom 2 ℤ/2 RP²  fst ℤ/2
H²[RP²,ℤ/2]→ℤ/2 =
  ST.rec isSetFin
    λ f  ΩEM+1→EM-gen 0 _
      (cong (ΩEM+1→EM-gen 1 _)
      ((cong (cong f) square  symConst-ℤ/2 2 _ (sym (cong f line)))))

ℤ/2→H²[RP²,ℤ/2] : fst ℤ/2  coHom 2 ℤ/2 RP²
ℤ/2→H²[RP²,ℤ/2] x =  RP²Fun (0ₖ 2) refl (Iso.inv Iso-Ω²K₂-ℤ/2 x) ∣₂

H²[RP²,ℤ/2]→ℤ/2-Id : (p : fst ((Ω^ 2) (EM∙ ℤ/2 2)))
                   H²[RP²,ℤ/2]→ℤ/2  RP²Fun (0ₖ 2) refl p ∣₂
                   Iso.fun Iso-Ω²K₂-ℤ/2 p
H²[RP²,ℤ/2]→ℤ/2-Id q = cong (Iso.fun Iso-Ω²K₂-ℤ/2) lem
  where
  lem : q  symConst-ℤ/2 2 _ refl  q
  lem =  i  q  transportRefl refl i)
        sym (rUnit q)

ℤ/2→H²[RP²,ℤ/2]→ℤ/2 : (x : fst ℤ/2)
   H²[RP²,ℤ/2]→ℤ/2 (ℤ/2→H²[RP²,ℤ/2] x)  x
ℤ/2→H²[RP²,ℤ/2]→ℤ/2 x =
    H²[RP²,ℤ/2]→ℤ/2-Id (Iso.inv Iso-Ω²K₂-ℤ/2 x)
   Iso.rightInv Iso-Ω²K₂-ℤ/2 x

H²[RP²,ℤ/2]→ℤ/2→H²[RP²,ℤ/2] : (x : coHom 2 ℤ/2 RP²)
   ℤ/2→H²[RP²,ℤ/2] (H²[RP²,ℤ/2]→ℤ/2 x)  x
H²[RP²,ℤ/2]→ℤ/2→H²[RP²,ℤ/2] =
  ST.elim  _  isSetPathImplicit)
    (RP²Conn.elim₂
      (isConnectedEM 2)
       _  squash₂ _ _)
      (0ₖ 2)
      λ sq  cong (ℤ/2→H²[RP²,ℤ/2])
               (H²[RP²,ℤ/2]→ℤ/2-Id sq)
             cong ∣_∣₂ (cong (RP²Fun (snd (EM∙ ℤ/2 2)) refl)
               (Iso.leftInv Iso-Ω²K₂-ℤ/2 sq)))

H²[RP²,ℤ/2]≅ℤ/2 : AbGroupEquiv (coHomGr 2 ℤ/2 RP²) ℤ/2
fst H²[RP²,ℤ/2]≅ℤ/2 = isoToEquiv is
  where
  is : Iso _ _
  Iso.fun is = H²[RP²,ℤ/2]→ℤ/2
  Iso.inv is = ℤ/2→H²[RP²,ℤ/2]
  Iso.rightInv is = ℤ/2→H²[RP²,ℤ/2]→ℤ/2
  Iso.leftInv is = H²[RP²,ℤ/2]→ℤ/2→H²[RP²,ℤ/2]
snd H²[RP²,ℤ/2]≅ℤ/2 =
  Isoℤ/2-morph (fst H²[RP²,ℤ/2]≅ℤ/2)
    _ (sym (H²[RP²,ℤ/2]→ℤ/2-Id refl)
      cong (H²[RP²,ℤ/2]→ℤ/2  ∣_∣₂)
            (characRP²Fun  _  0ₖ 2)))
       _ _ (funExt (ST.elim  _  isSetPathImplicit)
             λ f  cong ∣_∣₂ (funExt
               λ x  sym (-ₖConst-ℤ/2 1 (f x))))) _


----- Hⁿ(RP²,G), n ≥ 3 -----
H³⁺ⁿ[RP²,G]≅G : (n : ) (G : AbGroup )
   AbGroupEquiv (coHomGr (3 +ℕ n) G RP²) (trivialAbGroup {})
fst (H³⁺ⁿ[RP²,G]≅G n G) =
  isoToEquiv (isContr→Iso
    ( RP²Fun (0ₖ (3 +ℕ n)) refl refl ∣₂
    , (ST.elim  _  isSetPathImplicit)
       (RP²Conn.elim₃
         (isConnectedSubtr 4 n
           (subst  x  isConnected x (EM G (3 +ℕ n)))
             (+-comm 4 n)
             (isConnectedEM (3 +ℕ n))))
          _  squash₂ _ _)
         (0ₖ (3 +ℕ n))
         (cong ∣_∣₂ (characRP²Fun  _  0ₖ (3 +ℕ n)))))))
    isContrUnit*)
snd (H³⁺ⁿ[RP²,G]≅G n G) = makeIsGroupHom λ _ _  refl


---- H¹(RP², G) -----
H⁰[RP²,G]≅G :  {} (G : AbGroup )
   AbGroupEquiv (coHomGr 0 G RP²) G
H⁰[RP²,G]≅G G =
  H⁰conn ( point ∣ₕ , TR.elim  _  isOfHLevelPath 2 (isOfHLevelTrunc 2) _ _)
         (elimPropRP²  _  isOfHLevelTrunc 2 _ _) refl)) G

----- H¹(RP², G) ------
module _ { : Level} (G : AbGroup ) where
  private
    G[2]path : (x : (G [ 2 ]ₜ) .fst)  _+_ (snd G) (fst x) (fst x)  0g (snd G)
    G[2]path (x , p) = cong (_+_ (snd G) x) (sym (+IdR (snd G) x))  p

    G[2]path' : (x : (G [ 2 ]ₜ) .fst)   fst x  -_ (snd G) (fst x)
    G[2]path' x = (sym (+IdR (snd G) _)
                 cong (_+_ (snd G) (fst x)) (sym (+InvR (snd G) (fst x)))
                 (+Assoc (snd G) _ _ _))
               ∙∙ cong  w  _+_ (snd G) w (-_ (snd G) (fst x))) (G[2]path x)
               ∙∙ +IdL (snd G) _

  H¹[RP²,G]→G[2] : coHom 1 G RP²  (G [ 2 ]ₜ) .fst
  H¹[RP²,G]→G[2] =
    ST.rec (is-set (snd (G [ 2 ]ₜ)))
      λ f  ΩEM+1→EM-gen {G = G} 0 (f point) (cong f line)
          , cong (_+_ (snd G) (ΩEM+1→EM-gen 0 (f point) (cong f line)))
              (+IdR (snd G) _)
           sym (ΩEM+1→EM-gen-hom {G = G} 0 (f point) (cong f line) (cong f line))
           cong (ΩEM+1→EM-gen 0 (f point))
                 (sym (cong-∙ f line line)
                cong (cong f) (cong (line ∙_) square  rCancel line) )
           ΩEM+1→EM-gen-refl 0 (f point)

  G[2]→H¹[RP²,G] : (G [ 2 ]ₜ) .fst  coHom 1 G RP²
  G[2]→H¹[RP²,G] g =
      { point  embase
        ; (line i)  emloop (fst g) i
        ; (square i j) 
           (cong emloop (G[2]path' g)
           emloop-inv (AbGroup→Group G) (fst g)) i j }) ∣₂

  private
    G[2]≅H¹[RP²,G] : AbGroupEquiv (G [ 2 ]ₜ) (coHomGr 1 G RP²)
    fst G[2]≅H¹[RP²,G] = isoToEquiv (invIso is)
      where
      is : Iso _ _
      Iso.fun is =  H¹[RP²,G]→G[2]
      Iso.inv is =  G[2]→H¹[RP²,G]
      Iso.rightInv is (g , p) =
        Σ≡Prop  _  is-set (snd G) _ _)
        (Iso.leftInv (Iso-EM-ΩEM+1 0) g)
      Iso.leftInv is = ST.elim  _  isSetPathImplicit)
        (RP²Conn.elim₁ (isConnectedEM 1)  _  squash₂ _ _)
          embase
          λ p q  cong ∣_∣₂
            (funExt (elimSetRP²  _  emsquash _ _)
            refl
            (flipSquare (Iso.rightInv (Iso-EM-ΩEM+1 {G = G} 0) p)))))
    snd G[2]≅H¹[RP²,G] = makeIsGroupHom
      λ x y  cong ∣_∣₂
        (funExt (elimSetRP²  _  emsquash _ _) refl
          (flipSquare
            (EM→ΩEM+1-hom {G = G} 0 (fst x) (fst y)
             sym (cong₂+₁ (emloop (fst x)) (emloop (fst y)))))))


  H¹[RP²,G]≅G[2] : AbGroupEquiv (coHomGr 1 G RP²) (G [ 2 ]ₜ)
  H¹[RP²,G]≅G[2] = invGroupEquiv G[2]≅H¹[RP²,G]

----- H²(RP², G) ------
module _ (G : AbGroup ) where
  private
    ΩEM+1→EM-sym' : (p : fst (Ω (EM∙ G 2)))
       ΩEM+1→EM 1 (sym p)  (-ₖ ΩEM+1→EM 1 p)
    ΩEM+1→EM-sym'  p =
      ΩEM+1→EM-sym (suc zero) p
         (sym (rUnitₖ 1 ((-ₖ ΩEM+1→EM 1 p)))
        ∙∙ cong ((-ₖ ΩEM+1→EM 1 p) +ₖ_) (sym (ΩEM+1→EM-sym (suc zero) refl))
        ∙∙ rUnitₖ 1 ((-ₖ ΩEM+1→EM 1 p)))

    ΩEM+1→EM-sym'-refl : ΩEM+1→EM-sym' refl  refl
    ΩEM+1→EM-sym'-refl =
       i  ΩEM+1→EM-sym (suc zero) refl  rUnit (sym (ΩEM+1→EM-sym (suc zero) refl)) (~ i))
       rCancel _

    G/2-ord2 : (x : fst (G /^ 2))  (- snd (G /^ 2)) x  x
    G/2-ord2 = SQ.elimProp  _  SQ.squash/ _ _)
      λ a  eq/ _ _  snd G .-_ a
                    , cong (snd G ._+_ (snd G .-_ a)) (+IdR (snd G) _) ∣₁

  open EM2 (G /^ 2) G/2-ord2
  killFirstCompIsoGen : (n : )
     Iso  (Σ[ x  EM G (2 +ℕ n) ] (Σ[ p  x  x ] p  sym p)) ∥₂
                        (Σ[ p  Ω (EM∙ G (2 +ℕ n)) .fst ] p  sym p) ∥₂
  Iso.fun (killFirstCompIsoGen n) =
    ST.rec squash₂
      (uncurry (TR.elim  _  isOfHLevelPlus {n = 2 +ℕ n} 2
        (isOfHLevelPlus' {n = n} 2 (isSetΠ λ _  squash₂)))
        (EM-raw'-trivElim G (suc n)
           _  isOfHLevelΠ (suc (suc n))
            λ _  isOfHLevelPlus' {n = n} 2 squash₂) ∣_∣₂)))
  Iso.inv (killFirstCompIsoGen n) = ST.map (0ₖ (2 +ℕ n) ,_)
  Iso.rightInv (killFirstCompIsoGen n) = ST.elim  _  isSetPathImplicit) λ _  refl
  Iso.leftInv (killFirstCompIsoGen n) = ST.elim  _  isSetPathImplicit)
    (uncurry (TR.elim  _  isProp→isOfHLevelSuc (3 +ℕ n)
                        (isPropΠ  _  squash₂ _ _)))
      (EM-raw'-trivElim G (suc n)  _  isProp→isOfHLevelSuc (suc n)
        (isPropΠ λ _  squash₂ _ _ ))
        λ _  refl)))

  H²RP²-Iso₁ : Iso (coHom 2 G RP²)  (Σ[ p  Ω (EM∙ G 2) .fst ] p  sym p) ∥₂
  H²RP²-Iso₁ = compIso (setTruncIso RP²FunCharacIso) (killFirstCompIsoGen 0)

  H²RP²-Iso₂ : Iso ((Σ[ p  Ω (EM∙ G 2) .fst ] p  sym p)) (Σ[ p  EM G 1 ] p  -ₖ p)
  H²RP²-Iso₂ = (Σ-cong-iso (invIso (Iso-EM-ΩEM+1 1))
    λ x  compIso (congIso (invIso (Iso-EM-ΩEM+1 1)))
            (equivToIso (compPathrEquiv (ΩEM+1→EM-sym' x))))

  RP²Fun-pres+ : (p q : (Ω^ 2) (EM∙ G 2) .fst) (x : _)
     RP²Fun _ _ p x +[ 2 ]ₖ RP²Fun _ _ q x  RP²Fun _ _ (p  q) x
  RP²Fun-pres+ p q point = refl
  RP²Fun-pres+ p q (line i) j = 0ₖ 2
  RP²Fun-pres+ p q (square i j) k =
    hcomp  r  λ {(i = i0)  lem3 k j r
                   ; (i = i1)  lem2 k (~ r) j
                   ; (j = i0)  p (i  ~ k) r
                   ; (j = i1)  p (~ i  k) (~ r)
                   ; (k = i0)  cong₂+₂ 0 (p i) (q i) (~ r) j
                   ; (k = i1)  lem1 _ refl p (sym q) r i j})
          ((p i  q i) j)
    where
    lem1 :  {} {A : Type } (x : A) (p : x  x) (P Q : refl  p)
       Cube  i j  (P i  Q (~ i)) j) (P  sym Q)
               k  compPath-filler refl p (~ k))
               k  compPath-filler' p refl (~ k))
               i j  P j i) λ i j  P (~ j) (~ i)
    lem1 x = J> λ Q   i j k  lUnit (Q (~ j)) (~ i) k)  lUnit (sym Q)

    lem2 : cong₂+₂ {G = G} 0 refl refl  rUnit refl
    lem2 = sym (rUnit _)

    lem3 : Cube  j r  cong₂+₂ {G = G} 0 refl refl (~ r) j)
               j r  compPath-filler (refl {x = 0ₖ 2}) refl (~ r) j)
               k r  p (~ k) r)  k r  p k (~ r))
               j i  (rUnit (refl {x = 0ₖ 2}) i1) i)
               _ _  0ₖ 2)
    lem3 =  i j r  lem2 i (~ r) j)
        k j r 
        hcomp  i  λ {(j = i0)  p (~ k) r
                   ; (j = i1)  p k (~ r)
                   ; (r = i0)  rUnit  _  0ₖ 2) i j
                   ; (r = i1)  0ₖ 2
                   ; (k = i0)  rUnit  _  0ₖ 2) (i  ~ r) j
                   ; (k = i1)  rUnit  _  0ₖ 2) (i  ~ r) j})
         (((sym≡flipSquare p)  flipSquare≡cong-sym p) j k r))

  H²RP²-Iso₁,₂-charac : (p : (Ω^ 2) (EM∙ G 2) .fst)
     ST.map (Iso.fun H²RP²-Iso₂) (Iso.fun H²RP²-Iso₁  RP²Fun _ _ p ∣₂)
       embase , (cong (ΩEM+1→EM 1) p) ∣₂
  H²RP²-Iso₁,₂-charac p = cong ∣_∣₂ (ΣPathP (refl
    ,  i  cong (ΩEM+1→EM {G = G} 1) p  ΩEM+1→EM-sym'-refl i)
      sym (rUnit (cong (ΩEM+1→EM 1) p))))

  H²RP²-Iso₁,₂+ : (p q : (Ω^ 2) (EM∙ G 2) .fst)
     ST.map (Iso.fun H²RP²-Iso₂) (Iso.fun H²RP²-Iso₁ ( RP²Fun _ _ p ∣₂ +ₕ  RP²Fun _ _ q ∣₂))
      embase , cong (ΩEM+1→EM 1) p   cong (ΩEM+1→EM 1) q ∣₂
  H²RP²-Iso₁,₂+ p q = cong (ST.map (Iso.fun H²RP²-Iso₂)  Iso.fun H²RP²-Iso₁)
    (cong ∣_∣₂ (funExt (RP²Fun-pres+ p q)))
     H²RP²-Iso₁,₂-charac (p  q)
     cong ∣_∣₂ (ΣPathP (refl , cong-∙ (ΩEM+1→EM 1) p q))

  H²RP²-Iso₃→ : (p : EM G 1)  (p  -[ 1 ]ₖ p)  fst (G /^ 2)
  H²RP²-Iso₃→ = EM1.elimSet (AbGroup→Group G)  _  isSetΠ λ _  squash/)
     p  [ ΩEM+1→EM 0 p ])
    λ g  toPathP (funExt λ q
       cong [_] (transportRefl _
                  cong (ΩEM+1→EM 0)
                    ((λ j  transp  i  Path (EM G 1) (emloop g (~ i  ~ j)) (emloop g (i  j))) j
                       (doubleCompPath-filler (emloop g) q (emloop g) j))
                   doubleCompPath≡compPath _ _ _
                   cong (emloop g ∙_) (isCommΩEM {G = G} 0 q (emloop g))
                   assoc (emloop g) (emloop g) q)
                   ΩEM+1→EM-hom 0 (emloop g  emloop g) q)
                eq/ _ _  g
                       , cong (snd G ._+_ g) (+IdR (snd G) _)
                         sym (+IdR (snd G) (snd G ._+_ g g))
                         cong₂ (snd G ._+_)
                            (sym (Iso.leftInv (Iso-EM-ΩEM+1 0) _)
                              cong (ΩEM+1→EM 0) (emloop-comp _ g g))
                            (sym (+InvR (snd G) (ΩEM+1→EM 0 q)))
                         +Assoc (snd G) _ _ _ ∣₁)

  H²RP²-Iso₃ : Iso  (Σ[ p  EM G 1 ] p  -ₖ p) ∥₂ (fst (G /^ 2))
  Iso.fun H²RP²-Iso₃ = ST.rec squash/ (uncurry H²RP²-Iso₃→)
  Iso.inv H²RP²-Iso₃ =
    SQ.elim  _  squash₂)  a   embase , emloop a ∣₂)
            λ a b  PT.rec (squash₂ _ _)
              (uncurry λ x y  cong ∣_∣₂ (ΣPathP ((emloop x)
              , compPathL→PathP
                (cong₂ _∙_ (sym (emloop-inv _ x))
                (cong (emloop a ∙_) (sym (emloop-inv _ x))
                 sym (EM→ΩEM+1-hom {G = G} 0 a (AbGroupStr.-_ (snd G) x)))
                 sym (EM→ΩEM+1-hom {G = G} 0 _ _)
                 cong emloop (cong (_+_ (snd G) (AbGroupStr.-_ (snd G) x))
                              (+Comm (snd G) _ _)
                 +Assoc (snd G) _ _ _
                 cong  w  _+_ (snd G) w a)
                    (sym (GroupTheory.invDistr (AbGroup→Group G) x x)
                    cong (AbGroupStr.-_ (snd G))
                     (cong (snd G ._+_ x ) (sym (+IdR (snd G) _))  y)
                    GroupTheory.invDistr (AbGroup→Group G) a _
                    cong  w  _+_ (snd G) w (AbGroupStr.-_ (snd G) a))
                          (GroupTheory.invInv (AbGroup→Group G) b))
                 (sym (+Assoc (snd G) _ _ _)
                 cong (_+_ (snd G) b) (+InvL (snd G) a))
                 +IdR (snd G) b)))))
  Iso.rightInv H²RP²-Iso₃ = SQ.elimProp  _  squash/ _ _)
    λ a  cong [_] (Iso.leftInv (Iso-EM-ΩEM+1 0) a)
  Iso.leftInv H²RP²-Iso₃ = ST.elim  _  isSetPathImplicit)
    (uncurry (EM1.elimProp (AbGroup→Group G)  _  isPropΠ λ _  squash₂ _ _)
      λ p  cong ∣_∣₂ (ΣPathP (refl , (Iso.rightInv (Iso-EM-ΩEM+1 0) p)))))

  H²[RP²,G]≅G/2 : AbGroupEquiv (coHomGr 2 G RP²) (G /^ 2)
  fst H²[RP²,G]≅G/2 = isoToEquiv is
    where
    is : Iso _ _
    is = compIso (compIso H²RP²-Iso₁ (setTruncIso H²RP²-Iso₂)) H²RP²-Iso₃
  snd H²[RP²,G]≅G/2 =
    makeIsGroupHom (ST.elim2  _ _  isOfHLevelPath 2 squash/ _ _)
      (RP²Conn.elim₂ (isConnectedEM 2)  _  isPropΠ λ _  squash/ _ _)
        (0ₖ 2) λ p  RP²Conn.elim₂ (isConnectedEM 2)  _  squash/ _ _)
        (0ₖ 2) λ q  cong (Iso.fun H²RP²-Iso₃) (H²RP²-Iso₁,₂+ p q)
                    cong [_] (ΩEM+1→EM-hom 0 (cong (ΩEM+1→EM 1) p)
                                              (cong (ΩEM+1→EM 1) q))
                    cong₂ ((G /^ 2) .snd ._+_)
                       (cong (Iso.fun H²RP²-Iso₃) (sym (H²RP²-Iso₁,₂-charac p)))
                       (cong (Iso.fun H²RP²-Iso₃) (sym (H²RP²-Iso₁,₂-charac q)))))

  H³⁺ⁿ[RP²,G]≅0 : (n : )  AbGroupEquiv (coHomGr (3 +ℕ n) G RP²) (trivialAbGroup {})
  fst (H³⁺ⁿ[RP²,G]≅0 n) = isContr→≃Unit* (0ₕ _
                        , ST.elim  _  isSetPathImplicit)
                         (RP²Conn.elim₃ (isConnectedSubtr 4 n
                           (subst  k  isConnected k (EM G (3 +ℕ n)))
                                  (+-comm 4 n) (isConnectedEM (3 +ℕ n))))
                              _  squash₂ _ _) (0ₖ _) refl))
  snd (H³⁺ⁿ[RP²,G]≅0 n) = makeIsGroupHom λ _ _  refl