A type is acyclic if and only if its terminal map is an acyclic map (#…

…905)

src/foundation/fibers-of-maps.lagda.md

@@ -10,7 +10,10 @@ open import foundation-core.fibers-of-maps public
 
 ```agda
 open import foundation.cones-over-cospans
+open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.type-arithmetic-unit-type
 open import foundation.unit-type
 open import foundation.universe-levels
@@ -58,6 +61,53 @@ module _
         ( is-pullback-cone-fiber)
 ```
 
+### The fiber of the terminal map at any point is equivalent to its domain
+
+```agda
+module _
+  {l : Level} {A : UU l}
+  where
+
+  equiv-fiber-terminal-map :
+    (u : unit) → fiber (terminal-map {A = A}) u ≃ A
+  equiv-fiber-terminal-map u =
+    right-unit-law-Σ-is-contr
+      ( λ a → is-prop-is-contr is-contr-unit (terminal-map a) u)
+
+  inv-equiv-fiber-terminal-map :
+    (u : unit) → A ≃ fiber (terminal-map {A = A}) u
+  inv-equiv-fiber-terminal-map u =
+    inv-equiv (equiv-fiber-terminal-map u)
+
+  equiv-fiber-terminal-map-star :
+    fiber (terminal-map {A = A}) star ≃ A
+  equiv-fiber-terminal-map-star = equiv-fiber-terminal-map star
+
+  inv-equiv-fiber-terminal-map-star :
+    A ≃ fiber (terminal-map {A = A}) star
+  inv-equiv-fiber-terminal-map-star =
+    inv-equiv equiv-fiber-terminal-map-star
+```
+
+### The total space of the fibers of the terminal map is equivalent to its domain
+
+```agda
+module _
+  {l : Level} {A : UU l}
+  where
+
+  equiv-total-fiber-terminal-map :
+    Σ unit (fiber (terminal-map {A = A})) ≃ A
+  equiv-total-fiber-terminal-map =
+    ( left-unit-law-Σ-is-contr is-contr-unit star) ∘e
+    ( equiv-tot equiv-fiber-terminal-map)
+
+  inv-equiv-total-fiber-terminal-map :
+    A ≃ Σ unit (fiber (terminal-map {A = A}))
+  inv-equiv-total-fiber-terminal-map =
+    inv-equiv equiv-total-fiber-terminal-map
+```
+
 ## Table of files about fibers of maps
 
 The following table lists files that are about fibers of maps as a general

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

@@ -13,6 +13,7 @@ open import foundation.epimorphisms
 open import foundation.equivalences
 open import foundation.fibers-of-maps
 open import foundation.propositions
+open import foundation.unit-type
 open import foundation.universe-levels
 
 open import synthetic-homotopy-theory.acyclic-types
@@ -76,6 +77,24 @@ module _
             ( ac b)))
 ```
 
+### A type is acyclic if and only if its terminal map is an acyclic map
+
+```agda
+module _
+  {l : Level} (A : UU l)
+  where
+
+  is-acyclic-map-terminal-map-is-acyclic :
+    is-acyclic A → is-acyclic-map (terminal-map {A = A})
+  is-acyclic-map-terminal-map-is-acyclic ac u =
+    is-acyclic-equiv (equiv-fiber-terminal-map u) ac
+
+  is-acyclic-is-acyclic-map-terminal-map :
+    is-acyclic-map (terminal-map {A = A}) → is-acyclic A
+  is-acyclic-is-acyclic-map-terminal-map ac =
+    is-acyclic-equiv inv-equiv-fiber-terminal-map-star (ac star)
+```
+
 ## See also
 
 - [Dependent epimorphisms](foundation.dependent-epimorphisms.md)