From 5713f859393173263cd2dd0ee9bd4658183ffb92 Mon Sep 17 00:00:00 2001
From: Raymond Baker <96847663+morphismz@users.noreply.github.com>
Date: Mon, 7 Aug 2023 00:21:29 -0600
Subject: [PATCH] suspension loop space adjunction (#688)

This pr contains:
- definition of the underlying map of the equivalance
- definition of the underlying map of the inverse

Proof that these maps are in fact inverses of each other must wait until
another pr since I first must formalize the dependent universal property
of suspensions
---
 .../suspensions-of-types.lagda.md             | 79 +++++++++++++++++++
 1 file changed, 79 insertions(+)

diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index a59d2c3c6f..666934f169 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -19,6 +19,7 @@ open import foundation.homotopies
 open import foundation.identity-systems
 open import foundation.identity-types
 open import foundation.structure-identity-principle
+open import foundation.transport
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.unit-type
 open import foundation.universal-property-unit-type
@@ -29,6 +30,8 @@ open import structured-types.pointed-maps
 open import structured-types.pointed-types
 
 open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.conjugation-loops
+open import synthetic-homotopy-theory.functoriality-loop-spaces
 open import synthetic-homotopy-theory.loop-spaces
 open import synthetic-homotopy-theory.pushouts
 open import synthetic-homotopy-theory.universal-property-pushouts
@@ -135,6 +138,20 @@ pr1 (suspension-Pointed-Type X) = suspension (type-Pointed-Type X)
 pr2 (suspension-Pointed-Type X) = N-susp
 ```
 
+#### Suspension structure induced by a pointed type
+
+```agda
+constant-suspension-structure-Pointed-Type :
+  {l1 l2 : Level} (X : UU l1) (Y : Pointed-Type l2) →
+  suspension-structure X (type-Pointed-Type Y)
+pr1 (constant-suspension-structure-Pointed-Type X Y) =
+  point-Pointed-Type Y
+pr1 (pr2 (constant-suspension-structure-Pointed-Type X Y)) =
+  point-Pointed-Type Y
+pr2 (pr2 (constant-suspension-structure-Pointed-Type X Y)) =
+  const X (point-Pointed-Type Y ＝ point-Pointed-Type Y) refl
+```
+
 ## Properties
 
 #### Characterization of equalities in `suspension-structure`
@@ -482,6 +499,68 @@ module _
         ( id))
 ```
 
+#### The underlying map of the equivalence
+
+```agda
+module _
+  {l1 l2 : Level} (X : Pointed-Type l1) (Y : Pointed-Type l2)
+  where
+
+  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))
+```
+
+#### The underlying map of the inverse of the equivalence
+
+The following function takes a map `X → Ω Y` and returns a suspension structure
+on `Y`.
+
+```agda
+module _
+  {l1 l2 : Level} (X : UU l1) (Y : Pointed-Type l2)
+  where
+  suspension-structure-map-into-Ω :
+    (X → type-Ω Y) → suspension-structure X (type-Pointed-Type Y)
+  pr1 (suspension-structure-map-into-Ω f) = point-Pointed-Type Y
+  pr1 (pr2 (suspension-structure-map-into-Ω f)) = point-Pointed-Type Y
+  pr2 (pr2 (suspension-structure-map-into-Ω f)) = f
+```
+
+The above plus the universal property of suspensions defines the inverse map. We
+use the universal property to define the inverse.
+
+```agda
+module _
+  {l1 l2 : Level} (X : Pointed-Type l1) (Y : Pointed-Type l2)
+  where
+
+  map-inv-equiv-susp-loop-adj :
+    (X →∗ Ω Y) → ((suspension-Pointed-Type X) →∗ Y)
+  pr1 (map-inv-equiv-susp-loop-adj f∗) =
+    map-inv-up-suspension
+      ( type-Pointed-Type X)
+      ( type-Pointed-Type Y)
+      ( suspension-structure-map-into-Ω
+        ( type-Pointed-Type X)
+        ( Y)
+        ( map-pointed-map f∗))
+  pr2 (map-inv-equiv-susp-loop-adj f∗) =
+    up-suspension-N-susp
+      ( type-Pointed-Type X)
+      ( type-Pointed-Type Y)
+      ( suspension-structure-map-into-Ω
+      ( type-Pointed-Type X)
+      ( Y)
+      ( map-pointed-map f∗))
+```
+
+We now show these maps are inverses of each other.
+
+[To Do]
+
 #### The equivalence between pointed maps out of the suspension of X and pointed maps into the loop space of Y
 
 ```agda