Higher cohomology groups of real projective plane (#861)

* remove bool import

* newline

* delete everything @:-)

* whitespace...

* Update 8-6-1.agda

* testing

* Application

* updated Trunc

* move some things into ZCohomology.Properties + comments

* K-algebra

* K algebra laws done

* smash sphere

* push

* smash-assoc

* K-grousp

* K-alg

* whitespace etc

* merge main

* minor fixes

* delete abgroup

* rename

* renaming

* whitespace...

* MVunreduced

* MV-almostDone

* MV done

* finalbackup

* backup before merge

* injectivity

* cohom1-S1

* S1-done

* basechange-morph

* cohom1Torus-maps+rinv

* moreTorusStuff

* newBranchBackup

* moreCopatterns

* coHom-restructuring

* backup_before_merge

* private

* emptylines

* whitespace:-)

* backup

* last fixes

* merge

* whiteSpaceFiller3

* whiteSpaceFiller4

* fixes

* anders+whitespace

* fixes

* h1-sn

* cleanup

* cleanup2

* cleanup

* Benchmarks updated

* done

Co-authored-by: Axel Ljungström <axlj4439@r11a.math.su.se>
Co-authored-by: aljungstrom <axel.ljungstrom@math.su.se>

Cubical/ZCohomology/Groups/RP2.agda

@@ -12,7 +12,8 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
 
 open import Cubical.Data.Bool
-open import Cubical.Data.Int
+open import Cubical.Data.Nat
+open import Cubical.Data.Int hiding (_+_)
 open import Cubical.Data.Sigma
 
 open import Cubical.Algebra.Group
@@ -132,3 +133,33 @@ H²-RP²≅Bool = invGroupIso (≅Bool (compIso
                                     (compIso (setTruncIso funSpaceIso-RP²)
                                              Iso-H²-RP²₁)
                                     Iso-H²-RP²₂))
+
+-- Higher groups
+Hⁿ-RP²Contr : (n : ℕ) → isContr (coHom (3 + n) RP²)
+Hⁿ-RP²Contr n =
+  subst isContr
+    (isoToPath (setTruncIso (invIso (funSpaceIso-RP²))))
+    (∣ c ∣₂ , c-id)
+  where
+  c : Σ[ x ∈ coHomK (3 + n) ] Σ[ p ∈ x ≡ x ] p ≡ sym p
+  c = (0ₖ _) , refl , refl
+
+  c-id : (p : ∥ _ ∥₂) → ∣ c ∣₂ ≡ p
+  c-id =
+    ST.elim (λ _ → isSetPathImplicit)
+      (uncurry (coHomK-elim _
+        (λ _ → isOfHLevelΠ (3 + n) λ _ → isProp→isOfHLevelSuc (2 + n) (squash₂ _ _))
+          (uncurry λ p q →
+            T.rec (isProp→isOfHLevelSuc (suc n) (squash₂ _ _)) (λ pp →
+              T.rec (isProp→isOfHLevelSuc n (squash₂ _ _))
+                (λ qq → cong ∣_∣₂ (ΣPathP (refl , ΣPathP (pp , qq))))
+                (isConnectedPathP _ {A = (λ i → pp i ≡ sym (pp i))}
+                  (isConnectedPath _
+                    (isConnectedPath _ (isConnectedKn (2 + n)) _ _) _ _)
+                      refl q .fst))
+              (Iso.fun (PathIdTruncIso _)
+                (isContr→isProp
+                  (isConnectedPath _ (isConnectedKn (2 + n)) _ _) ∣ refl ∣ ∣ p ∣)))))
+
+Hⁿ-RP²≅0 : (n : ℕ) → GroupIso (coHomGr (3 + n) RP²) (UnitGroup₀)
+Hⁿ-RP²≅0 n = contrGroupIsoUnit (Hⁿ-RP²Contr n)