Equivalences are closed under "transfinite composition" (#1117)

- if a sequential diagram consists of equivalences, then injection maps
into its colimit are also equivalences
- as a corollary, sequential colimits of sequential diagrams of
contractible types are contractible

Progress towards #1080

src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md

@@ -91,6 +91,9 @@ module _
       ( map-cocone-sequential-diagram (succ-ℕ n))
       ( map-sequential-diagram A n)
   coherence-cocone-sequential-diagram = pr2 c
+
+  first-map-cocone-sequential-diagram : family-sequential-diagram A 0 → X
+  first-map-cocone-sequential-diagram = map-cocone-sequential-diagram 0
 ```
 
 ### Homotopies of cocones under a sequential diagram

src/synthetic-homotopy-theory/sequential-diagrams.lagda.md

@@ -9,7 +9,9 @@ module synthetic-homotopy-theory.sequential-diagrams where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.equivalences
 open import foundation.universe-levels
 ```
 
@@ -88,6 +90,27 @@ module _
   pr2 postcomp-sequential-diagram n g x = map-sequential-diagram A n (g x)
 ```
 
+### A sequential diagram of contractible types consists of equivalences
+
+This is an easy corollary of the fact that every map between
+[contractible types](foundation-core.contractible-types.md) is an
+[equivalence](foundation-core.equivalences.md).
+
+```agda
+module _
+  {l1 : Level} {A : sequential-diagram l1}
+  where
+
+  is-equiv-sequential-diagram-is-contr :
+    ((n : ℕ) → is-contr (family-sequential-diagram A n)) →
+    (n : ℕ) → is-equiv (map-sequential-diagram A n)
+  is-equiv-sequential-diagram-is-contr contrs n =
+    is-equiv-is-contr
+      ( map-sequential-diagram A n)
+      ( contrs n)
+      ( contrs (succ-ℕ n))
+```
+
 ## References
 
 {{#bibliography}} {{#reference SDR20}}