Refactor shift, pointed identity types are loop spaces (#727)

This pr does two related things: (i) it shows that pointed identity types are equivalent to loop spaces. this will be useful in the Eckmann-Hilton and Hopf proof (issue #702), since we can construct an eckmann-hilton term of type $s \cdot s = s \cdot s$, where `s` is the generator of $\Omega^2 \mathbb{S}^2$`. Then, using this equivalence, we get a term of type $\Omega^3 \mathbb{S}^2$. Due to the way the equivalence is defined, we will get many nice functoriality properties. In particular, the equivalence preserves path concatination. This will be helpful in the proof. It will also later be helpful when applying sypllepsis. (ii) the pr uses the above equivalenecs to replace `unshift` in the file `universal-property-suspensions-pointed-types` --------- Co-authored-by: Fredrik Bakke <[email protected]>
UniMath · Sep 10, 2023 · 91a0219 · 91a0219
1 parent 63d35ec
commit 91a0219
Show file tree

Hide file tree

Showing 4 changed files with 139 additions and 56 deletions.
diff --git a/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md
@@ -8,14 +8,18 @@ module synthetic-homotopy-theory.double-loop-spaces where
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.interchange-law
 open import foundation.path-algebra
 open import foundation.universe-levels
 
+open import structured-types.pointed-equivalences
 open import structured-types.pointed-types
 
+open import synthetic-homotopy-theory.functoriality-loop-spaces
 open import synthetic-homotopy-theory.iterated-loop-spaces
+open import synthetic-homotopy-theory.loop-spaces
 ```
 
 </details>
@@ -118,3 +122,18 @@ interchange-concat-Ω² :
 interchange-concat-Ω² =
   interchange-law-commutative-and-associative _∙_ eckmann-hilton-Ω² assoc
 ```
+
+### The loop space of a pointed type is equivalent to a double loop space
+
+```agda
+module _
+  {l : Level} {A : Pointed-Type l} {x : type-Pointed-Type A}
+  (p : point-Pointed-Type A ＝ x)
+  where
+
+  pointed-equiv-2-loop-pointed-identity :
+    Ω (pair (point-Pointed-Type A ＝ x) p) ≃∗ Ω² A
+  pointed-equiv-2-loop-pointed-identity =
+    pointed-equiv-Ω-pointed-equiv
+      ( pointed-equiv-loop-pointed-identity A p)
+```
diff --git a/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md
@@ -16,6 +16,7 @@ open import foundation.identity-types
 open import foundation.universe-levels
 
 open import structured-types.faithful-pointed-maps
+open import structured-types.pointed-equivalences
 open import structured-types.pointed-maps
 open import structured-types.pointed-types
 
@@ -95,3 +96,62 @@ module _
       ( pointed-map-faithful-pointed-map f)
       ( is-faithful-faithful-pointed-map f)
 ```
+
+### Pointed embeddings induce pointed equivalences on loop spaces
+
+```agda
+module _
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
+  (f : A →∗ B) (t : is-emb (map-pointed-map f))
+  where
+
+  is-equiv-map-Ω-emb :
+    is-equiv (map-Ω f)
+  is-equiv-map-Ω-emb =
+    is-equiv-comp
+      ( tr-type-Ω (preserves-point-pointed-map f))
+      ( ap (map-pointed-map f))
+      ( t (point-Pointed-Type A) (point-Pointed-Type A))
+      ( is-equiv-tr-type-Ω (preserves-point-pointed-map f))
+
+  equiv-map-Ω-emb :
+    type-Ω A ≃ type-Ω B
+  pr1 equiv-map-Ω-emb = map-Ω f
+  pr2 equiv-map-Ω-emb = is-equiv-map-Ω-emb
+
+  pointed-equiv-pointed-map-Ω-emb :
+    Ω A ≃∗ Ω B
+  pr1 pointed-equiv-pointed-map-Ω-emb = equiv-map-Ω-emb
+  pr2 pointed-equiv-pointed-map-Ω-emb = preserves-refl-map-Ω f
+```
+
+### the operator `pointed-map-Ω` preserves equivalences
+
+```agda
+module _
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
+  (e : A ≃∗ B)
+  where
+
+  equiv-map-Ω-pointed-equiv :
+    type-Ω A ≃ type-Ω B
+  equiv-map-Ω-pointed-equiv =
+    equiv-map-Ω-emb
+      ( pointed-map-pointed-equiv e)
+      ( is-emb-is-equiv (is-equiv-map-equiv-pointed-equiv e))
+```
+
+### `pointed-map-Ω` preserves pointed equivalences
+
+```agda
+module _
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
+  (e : A ≃∗ B)
+  where
+
+  pointed-equiv-Ω-pointed-equiv :
+    Ω A ≃∗ Ω B
+  pr1 pointed-equiv-Ω-pointed-equiv = equiv-map-Ω-pointed-equiv e
+  pr2 pointed-equiv-Ω-pointed-equiv =
+    preserves-refl-map-Ω (pointed-map-pointed-equiv e)
+```
diff --git a/src/synthetic-homotopy-theory/loop-spaces.lagda.md b/src/synthetic-homotopy-theory/loop-spaces.lagda.md
@@ -115,7 +115,8 @@ module _
   where
 
   associative-mul-Ω :
-    (x y z : type-Ω A) → Id (mul-Ω A (mul-Ω A x y) z) (mul-Ω A x (mul-Ω A y z))
+    (x y z : type-Ω A) →
+    Id (mul-Ω A (mul-Ω A x y) z) (mul-Ω A x (mul-Ω A y z))
   associative-mul-Ω x y z = assoc x y z
 ```
 
@@ -161,3 +162,21 @@ module _
     Id (tr-type-Ω p q) (inv p ∙ (q ∙ p))
   eq-tr-type-Ω refl q = inv right-unit
 ```
+
+## Properties
+
+### Every pointed identity type is equivalent to a loop space
+
+```agda
+module _
+  {l : Level} (A : Pointed-Type l) {x : type-Pointed-Type A}
+  (p : point-Pointed-Type A ＝ x)
+  where
+
+  pointed-equiv-loop-pointed-identity :
+    ( pair (point-Pointed-Type A ＝ x) p) ≃∗ Ω A
+  pr1 pointed-equiv-loop-pointed-identity =
+    equiv-concat' (point-Pointed-Type A) (inv p)
+  pr2 pointed-equiv-loop-pointed-identity =
+    right-inv p
+```
diff --git a/...thetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md b/...thetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md
@@ -67,72 +67,54 @@ module _
   {l1 : Level} (X : Pointed-Type l1)
   where
 
-  shift :
-    (type-Ω (suspension-Pointed-Type X)) → (north-suspension ＝ south-suspension)
-  shift l = l ∙ (meridian-suspension (point-Pointed-Type X))
-
-  shift∗ :
-    Ω (suspension-Pointed-Type X) →∗
-    (pair
-      ( north-suspension ＝ south-suspension)
-      (meridian-suspension (point-Pointed-Type X)))
-  pr1 shift∗ = shift
-  pr2 shift∗ = refl
-
-  unshift :
-    (north-suspension ＝ south-suspension) →
-    (type-Ω (suspension-Pointed-Type X))
-  unshift p = p ∙ inv (meridian-suspension (point-Pointed-Type X))
-
-  unshift∗ :
-    (pair
+  pointed-equiv-loop-pointed-identity-suspension :
+    ( pair
       ( north-suspension ＝ south-suspension)
-      ( meridian-suspension (point-Pointed-Type X))) →∗
-    Ω (suspension-Pointed-Type X)
-  pr1 unshift∗ = unshift
-  pr2 unshift∗ = right-inv (meridian-suspension (point-Pointed-Type X))
-
-  is-equiv-shift : is-equiv shift
-  is-equiv-shift =
-    is-equiv-concat'
-      ( north-suspension)
+      ( meridian-suspension (point-Pointed-Type X))) ≃∗
+    ( Ω (suspension-Pointed-Type X))
+  pointed-equiv-loop-pointed-identity-suspension =
+    pointed-equiv-loop-pointed-identity
+      ( suspension-Pointed-Type X)
       ( meridian-suspension (point-Pointed-Type X))
 
-  pointed-equiv-shift :
-    ( Ω (suspension-Pointed-Type X)) ≃∗
+  pointed-map-loop-pointed-identity-suspension :
     ( pair
       ( north-suspension ＝ south-suspension)
-      ( meridian-suspension (point-Pointed-Type X)))
-  pr1 (pr1 pointed-equiv-shift) = shift
-  pr2 (pr1 pointed-equiv-shift) = is-equiv-shift
-  pr2 pointed-equiv-shift = preserves-point-pointed-map shift∗
+      ( meridian-suspension (point-Pointed-Type X))) →∗
+    Ω (suspension-Pointed-Type X)
+  pointed-map-loop-pointed-identity-suspension =
+    pointed-map-pointed-equiv
+      ( pointed-equiv-loop-pointed-identity-suspension)
 
-  meridian-suspension∗ :
+  pointed-map-concat-meridian-suspension :
     X →∗
     ( pair
       ( north-suspension ＝ south-suspension)
       ( meridian-suspension (point-Pointed-Type X)))
-  pr1 meridian-suspension∗ = meridian-suspension
-  pr2 meridian-suspension∗ = refl
+  pr1 pointed-map-concat-meridian-suspension = meridian-suspension
+  pr2 pointed-map-concat-meridian-suspension = refl
 
-  unit-susp-loop-adj∗ : X →∗ Ω (suspension-Pointed-Type X)
-  unit-susp-loop-adj∗ = unshift∗ ∘∗ meridian-suspension∗
+  pointed-map-unit-susp-loop-adj : X →∗ Ω (suspension-Pointed-Type X)
+  pointed-map-unit-susp-loop-adj =
+    pointed-map-loop-pointed-identity-suspension ∘∗
+    pointed-map-concat-meridian-suspension
 
-  unit-susp-loop-adj : type-Pointed-Type X →
+  map-unit-susp-loop-adj : type-Pointed-Type X →
     type-Ω (suspension-Pointed-Type X)
-  unit-susp-loop-adj = map-pointed-map unit-susp-loop-adj∗
+  map-unit-susp-loop-adj = map-pointed-map pointed-map-unit-susp-loop-adj
 
-  counit-susp-loop-adj : (suspension (type-Ω X)) → type-Pointed-Type X
-  counit-susp-loop-adj =
+  map-counit-susp-loop-adj : (suspension (type-Ω X)) → type-Pointed-Type X
+  map-counit-susp-loop-adj =
     map-inv-is-equiv
       ( up-suspension (type-Ω X) (type-Pointed-Type X))
       ( ( point-Pointed-Type X) ,
         ( point-Pointed-Type X) ,
         ( id))
 
-  counit-susp-loop-adj∗ : ((suspension (type-Ω X)) , north-suspension) →∗ X
-  pr1 counit-susp-loop-adj∗ = counit-susp-loop-adj
-  pr2 counit-susp-loop-adj∗ =
+  pointed-map-counit-susp-loop-adj :
+    ( pair (suspension (type-Ω X)) north-suspension) →∗ X
+  pr1 pointed-map-counit-susp-loop-adj = map-counit-susp-loop-adj
+  pr2 pointed-map-counit-susp-loop-adj =
     up-suspension-north-suspension
       ( type-Ω X)
       ( type-Pointed-Type X)
@@ -151,7 +133,7 @@ module _
   map-equiv-susp-loop-adj :
     ((suspension-Pointed-Type X) →∗ Y) → (X →∗ Ω Y)
   map-equiv-susp-loop-adj f∗ =
-    ((pointed-map-Ω f∗) ∘∗ (unit-susp-loop-adj∗ X))
+    ((pointed-map-Ω f∗) ∘∗ (pointed-map-unit-susp-loop-adj X))
 ```
 
 #### The underlying map of the inverse equivalence
@@ -200,22 +182,25 @@ module _
           ( type-Pointed-Type Y)
           ( λ z → (point-Pointed-Type Y) ＝ z)
           ( λ t →
-            Σ ( type-Pointed-Type X → (point-Pointed-Type Y) ＝ (pr1 t))
+            Σ ( type-Pointed-Type X →
+                ( point-Pointed-Type Y) ＝ (pr1 t))
               ( λ f → f (point-Pointed-Type X) ＝ (pr2 t))))) ∘e
       ( ( equiv-tot (λ y1 → equiv-left-swap-Σ)) ∘e
         ( ( associative-Σ
             ( type-Pointed-Type Y)
-            ( λ y1 → type-Pointed-Type X → (point-Pointed-Type Y) ＝ y1)
+            ( λ y1 →
+              type-Pointed-Type X → point-Pointed-Type Y ＝ y1)
             ( λ z →
               Σ ( Id (point-Pointed-Type Y) (pr1 z))
                 ( λ x → pr2 z (point-Pointed-Type X) ＝ x))) ∘e
           ( ( inv-equiv
-              ( right-unit-law-Σ-is-contr
-                ( λ ( z : Σ ( type-Pointed-Type Y)
-                            ( λ y1 →
-                              type-Pointed-Type X →
-                              point-Pointed-Type Y ＝ y1)) →
-                  is-contr-total-path ((pr2 z) (point-Pointed-Type X))))) ∘e
+            ( right-unit-law-Σ-is-contr
+              ( λ ( z : Σ ( type-Pointed-Type Y)
+                ( λ y1 →
+                  type-Pointed-Type X →
+                  point-Pointed-Type Y ＝ y1)) →
+                    ( is-contr-total-path
+                      ( (pr2 z) (point-Pointed-Type X)))))) ∘e
             ( ( left-unit-law-Σ-is-contr
                 ( is-contr-total-path' (point-Pointed-Type Y))
                 ( (point-Pointed-Type Y) , refl)) ∘e