Suspensions increase connectedness and relating k-acyclic maps, k…

…-equivalences and `k`-connected maps (#951)

src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md

@@ -227,7 +227,7 @@ is a `k`-epi, by considering the commutative diagram for any `k`-type `X`:
 ```text
            horizontal-map-cocone (fst)
  (B → X) <---------------------------- cocone f f X
-    |                  ≃                  |
+    |                  ≃                  ^
  id | ≃                                 ≃ | (universal property)
     v                                     |
  (B → X) ------------------------> (pushout f f → X)

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

@@ -10,6 +10,8 @@ module synthetic-homotopy-theory.suspensions-of-types where
 open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.commuting-squares-of-identifications
+open import foundation.connected-types
+open import foundation.constant-maps
 open import foundation.contractible-types
 open import foundation.dependent-identifications
 open import foundation.dependent-pair-types
@@ -22,7 +24,11 @@ open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.path-algebra
+open import foundation.torsorial-type-families
 open import foundation.transport-along-identifications
+open import foundation.truncated-types
+open import foundation.truncation-levels
+open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.unit-type
 open import foundation.universe-levels
 
@@ -511,3 +517,74 @@ is-contr-suspension-is-contr {l} {X} is-contr-X =
       ( up-pushout terminal-map terminal-map))
     ( is-contr-unit)
 ```
+
+### Suspensions increase connectedness
+
+More precisely, the suspension of a `k`-connected type is `(k+1)`-connected.
+
+For the proof we use that a type `A` is `n`-connected if and only if the
+constant map `B → (A → B)` is an equivalence for all `n`-types `B`.
+
+So for any `(k+1)`-type `Y`, we have the commutative diagram
+
+```text
+                 const
+     Y ---------------------->  (suspension X → Y)
+     ^                                  |
+ pr1 | ≃                              ≃ | ev-suspension
+     |                      ≃           v
+  Σ (y y' : Y) , y ＝ y' <----- suspension-structure Y
+                                ≐ Σ (y y' : Y) , X → y ＝ y'
+```
+
+where the bottom map is induced by the equivalence `(y ＝ y') → (X → (y ＝ y'))`
+given by the fact that `X` is `k`-connected and `y ＝ y'` is a `k`-type.
+
+Since the left, bottom and right maps are equivalences, so is the top map, as
+desired.
+
+```agda
+module _
+  {l : Level} {k : 𝕋} {X : UU l}
+  where
+
+  is-equiv-north-suspension-ev-suspension-is-connected-Truncated-Type :
+    is-connected k X →
+    {l' : Level} (Y : Truncated-Type l' (succ-𝕋 k)) →
+    is-equiv
+      ( ( north-suspension-structure) ∘
+        ( ev-suspension
+          ( suspension-structure-suspension X)
+          ( type-Truncated-Type Y)))
+  is-equiv-north-suspension-ev-suspension-is-connected-Truncated-Type c Y =
+    is-equiv-comp
+      ( north-suspension-structure)
+      ( ev-suspension
+        ( suspension-structure-suspension X)
+        ( type-Truncated-Type Y))
+      ( is-equiv-ev-suspension
+        ( suspension-structure-suspension X)
+        ( up-pushout terminal-map terminal-map) (type-Truncated-Type Y))
+      ( is-equiv-pr1-is-contr
+        ( λ y →
+          is-torsorial-fiber-Id
+            ( λ y' →
+              ( const X (y ＝ y') ,
+                is-equiv-diagonal-is-connected (Id-Truncated-Type Y y y') c))))
+
+  is-connected-succ-suspension-is-connected :
+    is-connected k X → is-connected (succ-𝕋 k) (suspension X)
+  is-connected-succ-suspension-is-connected c =
+    is-connected-is-equiv-diagonal
+      ( λ Y →
+        is-equiv-right-factor
+          ( ( north-suspension-structure) ∘
+            ( ev-suspension
+              ( suspension-structure-suspension X)
+              ( type-Truncated-Type Y)))
+          ( const (suspension X) (type-Truncated-Type Y))
+          ( is-equiv-north-suspension-ev-suspension-is-connected-Truncated-Type
+              ( c)
+              ( Y))
+          ( is-equiv-id))
+```

src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md

@@ -27,6 +27,7 @@ open import foundation.precomposition-dependent-functions
 open import foundation.precomposition-functions
 open import foundation.propositions
 open import foundation.truncated-types
+open import foundation.truncation-equivalences
 open import foundation.truncation-levels
 open import foundation.type-arithmetic-unit-type
 open import foundation.unit-type
@@ -304,6 +305,35 @@ module _
         ( is-epimorphism-is-truncated-acyclic-map-Truncated-Type f af))
 ```
 
+### Every `k`-connected map is `(k+1)`-acyclic
+
+```agda
+module _
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  is-truncated-succ-acyclic-map-is-connected-map :
+    is-connected-map k f → is-truncated-acyclic-map (succ-𝕋 k) f
+  is-truncated-succ-acyclic-map-is-connected-map c b =
+    is-truncated-succ-acyclic-is-connected (c b)
+```
+
+### Every `k`-equivalence is `k`-acyclic
+
+```agda
+module _
+  {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  is-truncated-acyclic-map-is-truncation-equivalence :
+    is-truncation-equivalence k f → is-truncated-acyclic-map k f
+  is-truncated-acyclic-map-is-truncation-equivalence e =
+    is-truncated-acyclic-map-is-epimorphism-Truncated-Type f
+      ( λ C →
+        is-emb-is-equiv
+          ( is-equiv-precomp-is-truncation-equivalence k f e C))
+```
+
 ## See also
 
 - [Acyclic maps](synthetic-homotopy-theory.acyclic-maps.md)

src/synthetic-homotopy-theory/truncated-acyclic-types.lagda.md

@@ -83,6 +83,19 @@ module _
       ( ac)
 ```
 
+### Every `k`-connected type is `(k+1)`-acyclic
+
+```agda
+module _
+  {l : Level} {k : 𝕋} {A : UU l}
+  where
+
+  is-truncated-succ-acyclic-is-connected :
+    is-connected k A → is-truncated-acyclic (succ-𝕋 k) A
+  is-truncated-succ-acyclic-is-connected =
+    is-connected-succ-suspension-is-connected
+```
+
 ## See also
 
 - [Acyclic maps](synthetic-homotopy-theory.acyclic-maps.md)