Refactor shift, pointed identity types are loop spaces

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)
+```

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 equivalces 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)
+```

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
+```

src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md

@@ -67,56 +67,37 @@ 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) →∗
+  pointed-equiv-loop-pointed-identity-suspension :
     (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))
+      ( 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))
 
-  unshift∗ :
+  pointed-map-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))
-
-  pointed-equiv-shift :
-    ( Ω (suspension-Pointed-Type X)) ≃∗
-    ( 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∗
+  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∗
+  unit-susp-loop-adj∗ =
+    pointed-map-loop-pointed-identity-suspension ∘∗
+    pointed-map-concat-meridian-suspension
 
   unit-susp-loop-adj : type-Pointed-Type X →
     type-Ω (suspension-Pointed-Type X)
@@ -130,7 +111,8 @@ module _
         ( point-Pointed-Type X) ,
         ( id))
 
-  counit-susp-loop-adj∗ : ((suspension (type-Ω X)) , north-suspension) →∗ X
+  counit-susp-loop-adj∗ :
+    ( pair (suspension (type-Ω X)) north-suspension) →∗ X
   pr1 counit-susp-loop-adj∗ = counit-susp-loop-adj
   pr2 counit-susp-loop-adj∗ =
     up-suspension-north-suspension
@@ -200,12 +182,14 @@ 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
@@ -215,7 +199,8 @@ module _
                             ( λ y1 →
                               type-Pointed-Type X →
                               point-Pointed-Type Y ＝ y1)) →
-                  is-contr-total-path ((pr2 z) (point-Pointed-Type X))))) ∘e
+                  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