Characterization of acyclic types in terms of const to identity typ…

…es being an equivalence (#954)

src/foundation/constant-maps.lagda.md

@@ -10,6 +10,7 @@ open import foundation-core.constant-maps public
 
 ```agda
 open import foundation.0-maps
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.faithful-maps
 open import foundation.function-extensionality
@@ -23,6 +24,7 @@ open import foundation-core.embeddings
 open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
+open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.injective-maps
 open import foundation-core.propositional-maps
@@ -160,3 +162,18 @@ const-injection :
 pr1 (const-injection A B a) = const A B
 pr2 (const-injection A B a) = is-injective-const A B a
 ```
+
+### The action on identifications of a diagonal map is another diagonal map
+
+```agda
+htpy-diagonal-Id-ap-diagonal-htpy-eq :
+  {l1 l2 : Level} (A : UU l1) {B : UU l2} (x y : B) →
+  htpy-eq ∘ ap (const A B) {x} {y} ~ const A (x ＝ y)
+htpy-diagonal-Id-ap-diagonal-htpy-eq A x y refl = refl
+
+htpy-ap-diagonal-htpy-eq-diagonal-Id :
+  {l1 l2 : Level} (A : UU l1) {B : UU l2} (x y : B) →
+  const A (x ＝ y) ~ htpy-eq ∘ ap (const A B) {x} {y}
+htpy-ap-diagonal-htpy-eq-diagonal-Id A x y =
+  inv-htpy (htpy-diagonal-Id-ap-diagonal-htpy-eq A x y)
+```

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

@@ -7,6 +7,7 @@ module synthetic-homotopy-theory.acyclic-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.constant-maps
 open import foundation.contractible-maps
 open import foundation.contractible-types
@@ -17,9 +18,11 @@ open import foundation.embeddings
 open import foundation.epimorphisms
 open import foundation.equivalences
 open import foundation.fibers-of-maps
+open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.functoriality-dependent-function-types
 open import foundation.homotopies
+open import foundation.identity-types
 open import foundation.precomposition-dependent-functions
 open import foundation.precomposition-functions
 open import foundation.propositions
@@ -151,6 +154,52 @@ module _
             ( e X)))
 ```
 
+### A type is acyclic if and only if the constant map from any identity type is an equivalence
+
+More precisely, `A` is acyclic if and only if for all types `X` and elements
+`x,y : X`, the map
+
+```text
+ const : (x ＝ y) → (A → x ＝ y)
+```
+
+is an equivalence.
+
+```agda
+module _
+  {l : Level} (A : UU l)
+  where
+
+  is-equiv-const-Id-is-acyclic :
+    is-acyclic A →
+    {l' : Level} {X : UU l'} (x y : X) → is-equiv (const A (x ＝ y))
+  is-equiv-const-Id-is-acyclic ac {X = X} x y =
+    is-equiv-htpy
+      ( htpy-eq ∘ ap (const A X) {x} {y})
+      ( htpy-ap-diagonal-htpy-eq-diagonal-Id A x y)
+      ( is-equiv-comp
+        ( htpy-eq)
+        ( ap (const A X))
+        ( is-emb-const-is-acyclic A ac X x y)
+        ( funext (const A X x) (const A X y)))
+
+  is-acyclic-is-equiv-const-Id :
+    ({l' : Level} {X : UU l'} (x y : X) → is-equiv (const A (x ＝ y))) →
+    is-acyclic A
+  is-acyclic-is-equiv-const-Id h =
+    is-acyclic-is-emb-const A
+      ( λ X →
+        ( λ x y →
+          is-equiv-right-factor
+            ( htpy-eq)
+            ( ap (const A X))
+            ( funext (const A X x) (const A X y))
+            ( is-equiv-htpy
+              ( const A (x ＝ y))
+              ( htpy-diagonal-Id-ap-diagonal-htpy-eq A x y)
+              ( h x y))))
+```
+
 ### A map is acyclic if and only if it is an [dependent epimorphism](foundation.dependent-epimorphisms.md)
 
 The following diagram is a helpful illustration in the second proof:

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

@@ -7,6 +7,7 @@ module synthetic-homotopy-theory.truncated-acyclic-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.connected-maps
 open import foundation.connected-types
 open import foundation.constant-maps
@@ -17,9 +18,11 @@ open import foundation.embeddings
 open import foundation.epimorphisms-with-respect-to-truncated-types
 open import foundation.equivalences
 open import foundation.fibers-of-maps
+open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.functoriality-dependent-function-types
 open import foundation.homotopies
+open import foundation.identity-types
 open import foundation.precomposition-dependent-functions
 open import foundation.precomposition-functions
 open import foundation.propositions
@@ -159,6 +162,58 @@ module _
             ( e X)))
 ```
 
+### A type is `k`-acyclic if and only if the constant map from any identity type of any `k`-type is an equivalence
+
+More precisely, `A` is `k`-acyclic if and only if for all `k`-types `X` and
+elements `x,y : X`, the map
+
+```text
+ const : (x ＝ y) → (A → x ＝ y)
+```
+
+is an equivalence.
+
+```agda
+module _
+  {l : Level} {k : 𝕋} (A : UU l)
+  where
+
+  is-equiv-const-Id-is-acyclic-Truncated-Type :
+    is-truncated-acyclic k A →
+    {l' : Level} {X : Truncated-Type l' k} (x y : type-Truncated-Type X) →
+    is-equiv (const A (x ＝ y))
+  is-equiv-const-Id-is-acyclic-Truncated-Type ac {X = X} x y =
+    is-equiv-htpy
+      ( htpy-eq ∘ ap (const A (type-Truncated-Type X)) {x} {y})
+      ( htpy-ap-diagonal-htpy-eq-diagonal-Id A x y)
+      ( is-equiv-comp
+        ( htpy-eq)
+        ( ap (const A (type-Truncated-Type X)))
+        ( is-emb-const-is-truncated-acyclic-Truncated-Type A ac X x y)
+        ( funext
+          ( const A (type-Truncated-Type X) x)
+          ( const A (type-Truncated-Type X) y)))
+
+  is-truncated-acyclic-is-equiv-const-Id-Truncated-Type :
+    ( {l' : Level} {X : Truncated-Type l' k} (x y : type-Truncated-Type X) →
+      is-equiv (const A (x ＝ y))) →
+    is-truncated-acyclic k A
+  is-truncated-acyclic-is-equiv-const-Id-Truncated-Type h =
+    is-truncated-acyclic-is-emb-const-Truncated-Type A
+      ( λ X →
+        ( λ x y →
+          is-equiv-right-factor
+            ( htpy-eq)
+            ( ap (const A (type-Truncated-Type X)))
+            ( funext
+              ( const A (type-Truncated-Type X) x)
+              ( const A (type-Truncated-Type X) y))
+            ( is-equiv-htpy
+              ( const A (x ＝ y))
+              ( htpy-diagonal-Id-ap-diagonal-htpy-eq A x y)
+              ( h {X = X} x y))))
+```
+
 ### A map is `k`-acyclic if and only if it is an [dependent `k`-epimorphism](foundation.dependent-epimorphisms-with-respect-to-truncated-types.md)
 
 The proof is similar to that of dependent epimorphisms and