From 19567ecc6dcd67e7ef31477898655c4a5523aee2 Mon Sep 17 00:00:00 2001
From: VojtechStep <vojtechstepancik@outlook.com>
Date: Wed, 17 Apr 2024 20:48:26 +0200
Subject: [PATCH] Maps in sequential diagrams of contractibles are equivalences

---
 .../sequential-diagrams.lagda.md              | 23 +++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/src/synthetic-homotopy-theory/sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/sequential-diagrams.lagda.md
index 34fe7194f0..36b3ab63ed 100644
--- a/src/synthetic-homotopy-theory/sequential-diagrams.lagda.md
+++ b/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}}