{-# OPTIONS --lossy-unification #-}
module Cubical.ZCohomology.Groups.RP2 where

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

open import Cubical.Data.Bool
open import Cubical.Data.Nat
open import Cubical.Data.Int hiding (_+_)
open import Cubical.Data.Sigma

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.DirProd
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Bool
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.Group.Instances.Unit

open import Cubical.HITs.SetTruncation as ST
open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.Truncation as T
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.HITs.RPn.Base

open import Cubical.Homotopy.Connected

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.Groups.KleinBottle
open import Cubical.ZCohomology.Groups.Connected

private
  variable
    ℓ : Level
    A : Type ℓ



funSpaceIso-RP² : Iso (RP² → A) (Σ[ x ∈ A ] Σ[ p ∈ x ≡ x ] p ≡ sym p)
Iso.fun funSpaceIso-RP² f = f point , (cong f line , λ i j → f (square i j))
Iso.inv funSpaceIso-RP² (x , p , P) point = x
Iso.inv funSpaceIso-RP² (x , p , P) (line i) = p i
Iso.inv funSpaceIso-RP² (x , p , P) (square i j) = P i j
Iso.sec funSpaceIso-RP² (x , p , P) i = x , p , P
Iso.ret funSpaceIso-RP² f _ point = f point
Iso.ret funSpaceIso-RP² f _ (line i) = f (line i)
Iso.ret funSpaceIso-RP² f _ (square i j) = f (square i j)

private
  pathIso : {x : A} {p : x ≡ x} → Iso (p ≡ sym p) (p ∙ p ≡ refl)
  pathIso {p = p} = compIso (congIso (equivToIso (_ , compPathr-isEquiv p)))
                            (pathToIso (cong (p ∙ p ≡_) (lCancel p)))


--- H⁰(RP²) ≅ ℤ ----
connectedRP¹ : (x : RP²) → ∥ point ≡ x ∥₁
connectedRP¹ point = ∣ refl ∣₁
connectedRP¹ (line i) =
  isOfHLevel→isOfHLevelDep 1 {B = λ x → ∥ point ≡ x ∥₁}
    (λ _ → isPropPropTrunc) ∣ refl ∣₁ ∣ refl ∣₁ line i
connectedRP¹ (square i j) = helper i j
  where
  helper : SquareP (λ i j → ∥ point ≡ square i j ∥₁)
                   (isOfHLevel→isOfHLevelDep 1 {B = λ x → ∥ point ≡ x ∥₁}
                     (λ _ → isPropPropTrunc) ∣ refl ∣₁ ∣ refl ∣₁ line)
                   (symP (isOfHLevel→isOfHLevelDep 1 {B = λ x → ∥ point ≡ x ∥₁}
                           (λ _ → isPropPropTrunc) ∣ refl ∣₁ ∣ refl ∣₁ line))
                   refl refl
  helper = toPathP (isOfHLevelPathP 1 isPropPropTrunc _ _ _ _)


H⁰-RP²≅ℤ : GroupIso (coHomGr 0 RP²) ℤGroup
H⁰-RP²≅ℤ = H⁰-connected point connectedRP¹

--- H¹(RP²) ≅ 0 ----
isContr-H¹-RP²-helper : isContr ∥ Σ[ x ∈ coHomK 1 ] Σ[ p ∈ x ≡ x ] p ∙ p ≡ refl ∥₂
fst isContr-H¹-RP²-helper = ∣ 0ₖ 1 , refl , sym (rUnit refl) ∣₂
snd isContr-H¹-RP²-helper =
  ST.elim (λ _ → isOfHLevelPath 2 isSetSetTrunc _ _)
    (uncurry
      (T.elim (λ _ → isGroupoidΠ λ _ → isOfHLevelPlus {n = 1} 2 (isSetSetTrunc _ _))
      (toPropElim (λ _ → isPropΠ (λ _ → isSetSetTrunc _ _))
         λ {(p , nilp)
            → cong ∣_∣₂ (ΣPathP (refl , Σ≡Prop (λ _ → isOfHLevelTrunc 3 _ _ _ _)
                                         (rUnit refl
                                       ∙∙ cong (Kn→ΩKn+1 0) (sym (nilpotent→≡0 (ΩKn+1→Kn 0 p)
                                                                                 (sym (ΩKn+1→Kn-hom 0 p p)
                                                                                ∙ cong (ΩKn+1→Kn 0) nilp)))
                                       ∙∙ Iso.sec (Iso-Kn-ΩKn+1 0) p)))})))

H¹-RP²≅0 : GroupIso (coHomGr 1 RP²) UnitGroup₀
H¹-RP²≅0 =
  contrGroupIsoUnit
    (isOfHLevelRetractFromIso 0
      (setTruncIso (compIso funSpaceIso-RP²
                            (Σ-cong-iso-snd (λ _ → Σ-cong-iso-snd λ _ → pathIso))))
      isContr-H¹-RP²-helper)

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

Iso-H²-RP²₁ : Iso ∥ Σ[ x ∈ coHomK 2 ] Σ[ p ∈ x ≡ x ] p ≡ sym p ∥₂
                  ∥ Σ[ p ∈ 0ₖ 2 ≡ 0ₖ 2 ] p ≡ sym p ∥₂
Iso.fun Iso-H²-RP²₁ =
  ST.rec isSetSetTrunc
    (uncurry
      (T.elim (λ _ → is2GroupoidΠ λ _ → isOfHLevelPlus {n = 2} 2 isSetSetTrunc)
        (sphereElim _ (λ _ → isSetΠ (λ _ → isSetSetTrunc))
          λ p → ∣ fst p , snd p ∣₂)))
Iso.inv Iso-H²-RP²₁ = ST.map λ p → (0ₖ 2) , p
Iso.sec Iso-H²-RP²₁ = ST.elim (λ _ → isOfHLevelPath 2 isSetSetTrunc _ _)
                           λ _ → refl
Iso.ret Iso-H²-RP²₁ =
  ST.elim (λ _ → isOfHLevelPath 2 isSetSetTrunc _ _)
    (uncurry (T.elim (λ _ → is2GroupoidΠ λ _ → isOfHLevelPlus {n = 1} 3 (isSetSetTrunc _ _))
      (sphereToPropElim _ (λ _ → isPropΠ (λ _ → isSetSetTrunc _ _))
        λ p → refl)))

Iso-H²-RP²₂ : Iso ∥ Σ[ p ∈ 0ₖ 2 ≡ 0ₖ 2 ] p ≡ sym p ∥₂ Bool
Iso-H²-RP²₂ = compIso (setTruncIso (Σ-cong-iso-snd λ _ → pathIso))
                (compIso Iso-H²-𝕂²₂ testIso)


H²-RP²≅Bool : GroupIso (coHomGr 2 RP²) BoolGroup
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)