Equivalences are closed under "transfinite composition"

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}}