Long exact sequence of homotopy groups + Generator of π₃S²

Cubical/Foundations/GroupoidLaws.agda

@@ -190,12 +190,20 @@ doubleCompPath-elim' : {ℓ : Level} {A : Type ℓ} {w x y z : A} (p : w ≡ x)
                        (r : y ≡ z) → (p ∙∙ q ∙∙ r) ≡ p ∙ (q ∙ r)
 doubleCompPath-elim' p q r = (split-leftright' p q r) ∙ (sym (leftright p (q ∙ r)))
 
+cong-∙∙-filler : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {x y z w : A}
+     (f : A → B) (p : w ≡ x) (q : x ≡ y) (r : y ≡ z)
+  → I → I → I → B
+cong-∙∙-filler {A = A} f p q r k j i =
+  hfill ((λ k → λ { (j = i1) → doubleCompPath-filler (cong f p) (cong f q) (cong f r) k i
+                   ; (j = i0) → f (doubleCompPath-filler p q r k i)
+                   ; (i = i0) → f (p (~ k))
+                   ; (i = i1) → f (r k) }))
+    (inS (f (q i)))
+    k
+
 cong-∙∙ : ∀ {B : Type ℓ} (f : A → B) (p : w ≡ x) (q : x ≡ y) (r : y ≡ z)
           → cong f (p ∙∙ q ∙∙ r) ≡ (cong f p) ∙∙ (cong f q) ∙∙ (cong f r)
-cong-∙∙ f p q r j i = hcomp (λ k → λ { (j = i0) → f (doubleCompPath-filler p q r k i)
-                                     ; (i = i0) → f (p (~ k))
-                                     ; (i = i1) → f (r k) })
-                            (f (q i))
+cong-∙∙ f p q r j i = cong-∙∙-filler f p q r i1 j i
 
 cong-∙ : ∀ {B : Type ℓ} (f : A → B) (p : x ≡ y) (q : y ≡ z)
          → cong f (p ∙ q) ≡ (cong f p) ∙ (cong f q)

Cubical/Foundations/Pointed/Base.agda

@@ -32,6 +32,43 @@ idfun∙ : ∀ {ℓ} (A : Pointed ℓ) → A →∙ A
 idfun∙ A .fst x = x
 idfun∙ A .snd = refl
 
+{-Pointed equivalences -}
+_≃∙_ : ∀ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ') → Type (ℓ-max ℓ ℓ')
+A ≃∙ B = Σ[ e ∈ fst A ≃ fst B ] fst e (pt A) ≡ pt B
+
+invEquiv∙ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} → A ≃∙ B → B ≃∙ A
+fst (invEquiv∙ x) = invEquiv (fst x)
+snd (invEquiv∙ {A = A} x) =
+  sym (cong (fst (invEquiv (fst x))) (snd x)) ∙ retEq (fst x) (pt A)
+
+compEquiv∙ : ∀ {ℓ ℓ' ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+  → A ≃∙ B → B ≃∙ C → A ≃∙ C
+fst (compEquiv∙ e1 e2) = compEquiv (fst e1) (fst e2)
+snd (compEquiv∙ e1 e2) = cong (fst (fst e2)) (snd e1) ∙ snd e2
+
+Equiv∙J : ∀ {ℓ ℓ'} {B : Pointed ℓ} (C : (A : Pointed ℓ) → A ≃∙ B → Type ℓ')
+          → C B (idEquiv (fst B) , refl)
+          → {A : _} (e : A ≃∙ B) → C A e
+Equiv∙J {ℓ} {ℓ'} {B = B} C ind {A = A} =
+  uncurry λ e p → help e (pt A) (pt B) p C ind
+  where
+  help : ∀ {A : Type ℓ} (e : A ≃ typ B) (a : A) (b : typ B)
+       → (p : fst e a ≡ b)
+       → (C : (A : Pointed ℓ) → A ≃∙ (fst B , b) → Type ℓ')
+       → C (fst B , b) (idEquiv (fst B) , refl)
+       → C (A , a)  (e , p)
+  help = EquivJ (λ A e → (a : A) (b : typ B)
+       → (p : fst e a ≡ b)
+       → (C : (A : Pointed ℓ) → A ≃∙ (fst B , b) → Type ℓ')
+       → C (fst B , b) (idEquiv (fst B) , refl)
+       → C (A , a)  (e , p))
+        λ a b → J (λ b p
+          → (C : (A : Pointed ℓ) → A ≃∙ (fst B , b) → Type ℓ')
+                → C (fst B , b)
+      (idEquiv (fst B) , refl) →
+      C (typ B , a) (idEquiv (typ B) , p))
+         λ _ p → p
+
 ua∙ : ∀ {ℓ} {A B : Pointed ℓ} (e : fst A ≃ fst B)
                   → fst e (snd A) ≡ snd B → A ≡ B
 fst (ua∙ e p i) = ua e i

Cubical/Foundations/Pointed/Properties.agda

@@ -90,3 +90,10 @@ const∙ _ B .snd = refl
         (cong h (cong g f∙) ∙ cong h g∙) ∙ h∙
         ≡⟨ cong (λ p → p ∙ h∙) ((cong-∙ h (cong g f∙) g∙) ⁻¹) ⟩
         (cong h (cong g f∙ ∙ g∙) ∙ h∙) ∎ )
+
+module _ {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B) where
+  isInIm∙ : (x : typ B) → Type (ℓ-max ℓ ℓ')
+  isInIm∙ x = Σ[ z ∈ typ A ] fst f z ≡ x
+
+  isInKer∙ : (x : fst A) → Type ℓ'
+  isInKer∙ x = fst f x ≡ snd B

Cubical/Foundations/Prelude.agda

@@ -321,16 +321,31 @@ module _ {A : I → Type ℓ} {x : A i0} {y : A i1} where
   fromPathP p i = transp (λ j → A (i ∨ j)) i (p i)
 
 -- Whiskering a dependent path by a path
+-- Double whiskering
+_◁_▷_ : ∀ {ℓ} {A : I → Type ℓ} {a₀ a₀' : A i0} {a₁ a₁' : A i1}
+      → a₀ ≡ a₀' → PathP A a₀' a₁ → a₁ ≡ a₁'
+      → PathP A a₀ a₁'
+(p ◁ P ▷ q) i =
+  hcomp (λ j → λ {(i = i0) → p (~ j) ; (i = i1) → q j}) (P i)
+
+doubleWhiskFiller :
+  ∀ {ℓ} {A : I → Type ℓ} {a₀ a₀' : A i0} {a₁ a₁' : A i1}
+      → (p : a₀ ≡ a₀') (pq : PathP A a₀' a₁) (q : a₁ ≡ a₁')
+      → PathP (λ i → PathP A (p (~ i)) (q i))
+               pq
+               (p ◁ pq ▷ q)
+doubleWhiskFiller p pq q k i =
+  hfill (λ j → λ {(i = i0) → p (~ j) ; (i = i1) → q j})
+        (inS (pq i))
+        k
 
 _◁_ : ∀ {ℓ} {A : I → Type ℓ} {a₀ a₀' : A i0} {a₁ : A i1}
   → a₀ ≡ a₀' → PathP A a₀' a₁ → PathP A a₀ a₁
-(p ◁ q) i =
-  hcomp (λ j → λ {(i = i0) → p (~ j); (i = i1) → q i1}) (q i)
+(p ◁ q) = p ◁ q ▷ refl
 
 _▷_ : ∀ {ℓ} {A : I → Type ℓ} {a₀ : A i0} {a₁ a₁' : A i1}
   → PathP A a₀ a₁ → a₁ ≡ a₁' → PathP A a₀ a₁'
-(p ▷ q) i =
-  hcomp (λ j → λ {(i = i0) → p i0; (i = i1) → q j}) (p i)
+p ▷ q  = refl ◁ p ▷ q
 
 -- Direct definitions of lower h-levels
 

Cubical/HITs/SetTruncation/Base.agda

@@ -9,9 +9,15 @@ This file contains:
 module Cubical.HITs.SetTruncation.Base where
 
 open import Cubical.Core.Primitives
+open import Cubical.Foundations.Pointed
 
 -- set truncation as a higher inductive type:
 
 data ∥_∥₂ {ℓ} (A : Type ℓ) : Type ℓ where
   ∣_∣₂ : A → ∥ A ∥₂
   squash₂ : ∀ (x y : ∥ A ∥₂) (p q : x ≡ y) → p ≡ q
+
+-- Pointed version
+∥_∥₂∙ : ∀ {ℓ} (A : Pointed ℓ) → Pointed ℓ
+fst ∥ A ∥₂∙ = ∥ fst A ∥₂
+snd ∥ A ∥₂∙ = ∣ pt A ∣₂

Cubical/HITs/SetTruncation/Properties.agda

@@ -17,6 +17,7 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Pointed.Base
 open import Cubical.Data.Sigma
 open import Cubical.HITs.PropositionalTruncation
   renaming (rec to pRec ; elim to pElim) hiding (elim2 ; elim3 ; rec2 ; map)
@@ -203,6 +204,11 @@ module rec→Gpd {A : Type ℓ} {B : Type ℓ'} (Bgpd : isGroupoid B) (f : A →
 map : (A → B) → ∥ A ∥₂ → ∥ B ∥₂
 map f = rec squash₂ λ x → ∣ f x ∣₂
 
+map∙ : {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'}
+       (f : A →∙ B) → ∥ A ∥₂∙ →∙ ∥ B ∥₂∙
+fst (map∙ f) = map (fst f)
+snd (map∙ f) = cong ∣_∣₂ (snd f)
+
 setTruncUniversal : isSet B → (∥ A ∥₂ → B) ≃ (A → B)
 setTruncUniversal {B = B} Bset =
   isoToEquiv (iso (λ h x → h ∣ x ∣₂) (rec Bset) (λ _ → refl) rinv)

Cubical/Homotopy/Group/Base.agda

@@ -256,7 +256,7 @@ leftInv (SphereMapΩIso (suc n)) = rightInv IsoΩFunSuspFun
 In order to show that Ω→SphereMap is an equivalence, we show that it factors
 
              Ω→SphereMapSplit₁               ΩSphereMap
-Ωⁿ⁺¹(Sⁿ →∙ A) ----------------> Ω (Sⁿ →∙ A) -----------> (Sⁿ⁺¹ →∙ A)
+Ωⁿ⁺¹A ----------------> Ω (Sⁿ →∙ A) -----------> (Sⁿ⁺¹ →∙ A)
 -}
 
 Ω→SphereMap-split : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (p : typ ((Ω^ (suc n)) A))
@@ -772,15 +772,14 @@ hLevΩ+ {A = A} (suc n) (suc m) p =
     (hLevΩ+ {A = Ω A} (suc n) m
       (isOfHLevelPath' (m + suc n) p _ _))
 
-private
-  isSetΩ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
-    → (isSet (typ (Ω ((Ω^ n) (hLevelTrunc∙ (suc (suc (suc n))) A)))))
-  isSetΩ {A = A} zero = isOfHLevelTrunc 3 _ _
-  isSetΩ {A = A} (suc n) =
-    hLevΩ+ 2 (suc (suc n))
-      (transport
-       (λ i → isOfHLevel (+-comm 2 (2 + n) i) (hLevelTrunc (4 + n) (typ A)))
-        (isOfHLevelTrunc (suc (suc (suc (suc n))))))
+isSetΩTrunc : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
+  → (isSet (typ (Ω ((Ω^ n) (hLevelTrunc∙ (suc (suc (suc n))) A)))))
+isSetΩTrunc {A = A} zero = isOfHLevelTrunc 3 _ _
+isSetΩTrunc {A = A} (suc n) =
+  hLevΩ+ 2 (suc (suc n))
+    (transport
+     (λ i → isOfHLevel (+-comm 2 (2 + n) i) (hLevelTrunc (4 + n) (typ A)))
+      (isOfHLevelTrunc (suc (suc (suc (suc n))))))
 
 πTruncIso : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
              → Iso (π n A) (π n (hLevelTrunc∙ (2 + n) A))
@@ -791,7 +790,7 @@ private
   compIso setTruncTrunc2Iso
     (compIso
      (2TruncΩIso (suc n))
-     (invIso (setTruncIdempotentIso (isSetΩ n))))
+     (invIso (setTruncIdempotentIso (isSetΩTrunc n))))
 
 πTruncGroupIso : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
              → GroupIso (πGr n A) (πGr n (hLevelTrunc∙ (3 + n) A))
@@ -800,7 +799,7 @@ snd (πTruncGroupIso {A = A} n) =
   makeIsGroupHom
     (sElim2 (λ _ _ → isSetPathImplicit)
       λ a b
-      → cong (inv (setTruncIdempotentIso (isSetΩ n)))
+      → cong (inv (setTruncIdempotentIso (isSetΩTrunc n)))
          (cong
           (transport
            (λ i → typ ((Ω^ suc n) (hLevelTrunc∙ (+-comm (suc n) 2 i) A))))
@@ -820,3 +819,41 @@ snd (πTruncGroupIso {A = A} n) =
                ∙ subst (λ n → typ (Ω (A n))) r q)
       λ p q → transportRefl _ ∙ cong₂ _∙_
                 (sym (transportRefl p)) (sym (transportRefl q))
+
+π'fun : ∀ {ℓ} {A : Pointed ℓ} {B : Pointed ℓ} (n : ℕ)
+      → A ≃∙ B
+      → (π' (suc n) A) → π' (suc n) B
+π'fun n p = sMap ((fst (fst p) , snd p) ∘∙_)
+
+π'fun-idEquiv : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
+              → π'fun n (idEquiv (fst A) , (λ _ → pt A))
+              ≡ idfun _
+π'fun-idEquiv n =
+  funExt (sElim (λ _ → isSetPathImplicit)
+    λ f → cong ∣_∣₂ (∘∙-idʳ f))
+
+π'funIsEquiv :
+  ∀ {ℓ} {A : Pointed ℓ} {B : Pointed ℓ} (n : ℕ)
+      → (e : A ≃∙ B)
+      → isEquiv (π'fun n e)
+π'funIsEquiv {B = B} n =
+  Equiv∙J (λ A e → isEquiv (π'fun n e))
+    (subst isEquiv (sym (π'fun-idEquiv n))
+      (idIsEquiv (π' (suc n) B)))
+
+π'funIsHom : ∀ {ℓ} {A : Pointed ℓ} {B : Pointed ℓ} (n : ℕ)
+      → (e : A ≃∙ B)
+      → IsGroupHom (π'Gr n A .snd) (π'fun n e)
+                      (π'Gr n B .snd)
+π'funIsHom {B = B} n =
+  Equiv∙J (λ A e → IsGroupHom (π'Gr n A .snd) (π'fun n e) (π'Gr n B .snd))
+    (subst (λ x → IsGroupHom (π'Gr n B .snd) x (π'Gr n B .snd))
+      (sym (π'fun-idEquiv n))
+      (makeIsGroupHom λ _ _ → refl))
+
+π'Iso : ∀ {ℓ} {A : Pointed ℓ} {B : Pointed ℓ} (n : ℕ)
+      → A ≃∙ B
+      → GroupEquiv (π'Gr n A) (π'Gr n B)
+fst (fst (π'Iso n e)) = π'fun n e
+snd (fst (π'Iso n e)) = π'funIsEquiv n e
+snd (π'Iso n e) = π'funIsHom n e