------------------------------------------------------------------------
-- Homotopy groups of pointed types
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

import Equality.Path as P

module Pointed-type.Homotopy-group
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Equality.Groupoid equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J
open import Group equality-with-J as G using (Group; Abelian; _≃ᴳ_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation eq as T
open import Pointed-type equality-with-J as PT
  using (Pointed-type; _≃ᴮ_; Ω; Ω[_])

private
  variable
    a p q : Level
    P     : Pointed-type p
    n     : ℕ

-- Homotopy-group-[1+ n ] P is the (1+n)-th homotopy group of the
-- pointed type P.
--
-- This definition is taken from the HoTT book.

Homotopy-group-[1+_] : ℕ → Pointed-type a → Group a
Homotopy-group-[1+ n ] P = λ where
    .Group.Carrier        → Carrier
    .Group.Carrier-is-set → Carrier-is-set
    .Group._∘_            → _∘′_
    .Group.id             → id′
    .Group._⁻¹            → _⁻¹
    .Group.left-identity  → left-identity
    .Group.right-identity → right-identity
    .Group.assoc          → assoc
    .Group.left-inverse   → left-inverse
    .Group.right-inverse  → right-inverse
  where
  Carrier = ∥ proj₁ (Ω[ 1 + n ] P) ∥[1+ 1 ]
  _∘′_    = ∥∥-zip trans
  id′     = ∣ refl _ ∣
  _⁻¹     = ∥∥-map sym

  opaque

    Carrier-is-set : Is-set Carrier
    Carrier-is-set = truncation-has-correct-h-level 1

    left-identity : (x : Carrier) → (id′ ∘′ x) ≡ x
    left-identity = T.elim λ where
      .T.∣∣ʳ _      → cong ∣_∣ $ trans-reflˡ _
      .T.h-levelʳ _ → mono₁ 2 $ truncation-has-correct-h-level 1

    right-identity : (x : Carrier) → (x ∘′ id′) ≡ x
    right-identity = T.elim λ where
      .T.∣∣ʳ _      → cong ∣_∣ $ trans-reflʳ _
      .T.h-levelʳ _ → mono₁ 2 $ truncation-has-correct-h-level 1

    assoc : (x y z : Carrier) → (x ∘′ (y ∘′ z)) ≡ ((x ∘′ y) ∘′ z)
    assoc = T.elim λ where
      .T.h-levelʳ _ → Π-closure ext 2 λ _ →
                      Π-closure ext 2 λ _ →
                      mono₁ 2 $ truncation-has-correct-h-level 1
      .T.∣∣ʳ _      → T.elim λ where
        .T.h-levelʳ _ → Π-closure ext 2 λ _ →
                        mono₁ 2 $ truncation-has-correct-h-level 1
        .T.∣∣ʳ _      → T.elim λ where
          .T.h-levelʳ _ → mono₁ 2 $ truncation-has-correct-h-level 1
          .T.∣∣ʳ _      → cong ∣_∣ $ sym $ trans-assoc _ _ _

    left-inverse : (x : Carrier) → ((x ⁻¹) ∘′ x) ≡ id′
    left-inverse = T.elim λ where
      .T.∣∣ʳ _      → cong ∣_∣ $ trans-symˡ _
      .T.h-levelʳ _ → mono₁ 2 $ truncation-has-correct-h-level 1

    right-inverse : (x : Carrier) → (x ∘′ (x ⁻¹)) ≡ id′
    right-inverse = T.elim λ where
      .T.∣∣ʳ _      → cong ∣_∣ $ trans-symʳ _
      .T.h-levelʳ _ → mono₁ 2 $ truncation-has-correct-h-level 1

-- The fundamental group of a pointed type.
--
-- This definition is taken from the HoTT book.

Fundamental-group : Pointed-type a → Group a
Fundamental-group = Homotopy-group-[1+ 0 ]

-- The n-th homotopy group of a pointed type is abelian when n is at
-- least two.
--
-- (This result is stated in the HoTT book.)

abelian : ∀ n → Abelian (Homotopy-group-[1+ suc n ] P)
abelian n = T.elim λ where
  .T.h-levelʳ _ → Π-closure ext 2 λ _ →
                  mono₁ 2 $ truncation-has-correct-h-level 1
  .T.∣∣ʳ p      → T.elim λ where
    .T.h-levelʳ _ → mono₁ 2 $ truncation-has-correct-h-level 1
    .T.∣∣ʳ q      → cong ∣_∣ $ Ω[2+n]-commutative n p q

-- If there is a based equivalence between P and Q, then their
-- homotopy groups are isomorphic.

≃ᴮ→≃ᴳ :
  ∀ (P : Pointed-type p) (Q : Pointed-type q) n →
  P ≃ᴮ Q → Homotopy-group-[1+ n ] P ≃ᴳ Homotopy-group-[1+ n ] Q
≃ᴮ→≃ᴳ P Q n P≃Q = λ where
  .G.Homomorphic.related →
    ∥∥-cong (proj₁ (PT.Ω[ suc n ]-cong-≃ᴮ P≃Q))
  .G.Homomorphic.homomorphic → T.elim λ where
    .T.h-levelʳ _ → Π-closure ext 2 λ _ →
                    mono₁ 2 $ truncation-has-correct-h-level 1
    .T.∣∣ʳ _      → T.elim λ where
      .T.h-levelʳ _ → mono₁ 2 $ truncation-has-correct-h-level 1
      .T.∣∣ʳ _      → cong ∣_∣ (PT.Ω[1+ n ]-cong-≃ᴮ-trans P≃Q)

-- Homotopy-group-[1+ n ] commutes with PT._×_/G._×_.

Homotopy-group-[1+_]-× :
  ∀ n (P : Pointed-type p) (Q : Pointed-type q) →
  Homotopy-group-[1+ n ] (P PT.× Q) ≃ᴳ
  (Homotopy-group-[1+ n ] P G.× Homotopy-group-[1+ n ] Q)
Homotopy-group-[1+ n ]-× P Q = λ where
    .G.Homomorphic.related →
      ∥ proj₁ (Ω[ 1 + n ] (P PT.× Q)) ∥[1+ 1 ]                           ↝⟨ T.∥∥-cong (proj₁ PT.Ω[ 1 + n ]-×) ⟩
      ∥ proj₁ (Ω[ 1 + n ] P) × proj₁ (Ω[ 1 + n ] Q) ∥[1+ 1 ]             ↝⟨ inverse T.∥∥×∥∥≃∥×∥ ⟩□
      ∥ proj₁ (Ω[ 1 + n ] P) ∥[1+ 1 ] × ∥ proj₁ (Ω[ 1 + n ] Q) ∥[1+ 1 ]  □
    .G.Homomorphic.homomorphic → T.elim λ where
      .T.h-levelʳ _ → Π-closure ext 2 λ _ → s
      .T.∣∣ʳ p → T.elim λ where
        .T.h-levelʳ _ → s
        .T.∣∣ʳ q →
          Σ-map ∣_∣ ∣_∣ (_≃_.to (proj₁ PT.Ω[ 1 + n ]-×) (trans p q))  ≡⟨ cong (Σ-map ∣_∣ ∣_∣) PT.Ω[1+ n ]-×-trans ⟩∎

          (Σ-map ∣_∣ ∣_∣ $ Σ-zip trans trans
             (_≃_.to (proj₁ PT.Ω[ 1 + n ]-×) p)
             (_≃_.to (proj₁ PT.Ω[ 1 + n ]-×) q))                      ∎
  where
  s =
    mono₁ 2 $
    ×-closure 2
      (truncation-has-correct-h-level 1)
      (truncation-has-correct-h-level 1)

-- Homotopy-group-[1+ n ]′ P s is the (1+n)-th homotopy group of the
-- pointed type P.
--
-- The definition does not use set truncation. Instead a certain loop
-- space is required to be a set.

Homotopy-group-[1+_]′ :
  ∀ n (P : Pointed-type a) → Is-set (proj₁ (Ω[ 1 + n ] P)) → Group a
Homotopy-group-[1+ n ]′ P s = λ where
    .Group.Carrier        → Carrier
    .Group.Carrier-is-set → Carrier-is-set
    .Group._∘_            → _∘′_
    .Group.id             → id′
    .Group._⁻¹            → _⁻¹
    .Group.left-identity  → left-identity
    .Group.right-identity → right-identity
    .Group.assoc          → assoc
    .Group.left-inverse   → left-inverse
    .Group.right-inverse  → right-inverse
  where
  Carrier = proj₁ (Ω[ 1 + n ] P)
  _∘′_    = trans
  id′     = refl _
  _⁻¹     = sym

  opaque

    Carrier-is-set : Is-set Carrier
    Carrier-is-set = s

    left-identity : (x : Carrier) → (id′ ∘′ x) ≡ x
    left-identity _ = trans-reflˡ _

    right-identity : (x : Carrier) → (x ∘′ id′) ≡ x
    right-identity _ = trans-reflʳ _

    assoc : (x y z : Carrier) → (x ∘′ (y ∘′ z)) ≡ ((x ∘′ y) ∘′ z)
    assoc _ _ _ = sym $ trans-assoc _ _ _

    left-inverse : (x : Carrier) → ((x ⁻¹) ∘′ x) ≡ id′
    left-inverse _ = trans-symˡ _

    right-inverse : (x : Carrier) → (x ∘′ (x ⁻¹)) ≡ id′
    right-inverse _ = trans-symʳ _

-- The fundamental group of a pointed type.
--
-- The definition does not use set truncation. Instead a certain loop
-- space is required to be a set.

Fundamental-group′ :
  (P : Pointed-type a) → Is-set (proj₁ (Ω P)) → Group a
Fundamental-group′ = Homotopy-group-[1+ 0 ]′

-- Homotopy-group-[1+ n ]′ P s is isomorphic to
-- Homotopy-group-[1+ n ] P.

Homotopy-group-[1+]′≃ᴳHomotopy-group-[1+] :
  {s : Is-set (proj₁ (Ω[ 1 + n ] P))} →
  Homotopy-group-[1+ n ]′ P s ≃ᴳ Homotopy-group-[1+ n ] P
Homotopy-group-[1+]′≃ᴳHomotopy-group-[1+] {s} = λ where
  .G.Homomorphic.related →
    inverse $ Eq.↔⇒≃ $ _⇔_.to T.+⇔∥∥↔ (λ {_ _} → s)
  .G.Homomorphic.homomorphic p q →
    ∣ trans p q ∣  ≡⟨⟩
    ∣ trans p q ∣  ∎