Maps in sequential diagrams of contractibles are equivalences

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