Prose feedback

UniMath · Apr 6, 2024 · 33d3c0c · 33d3c0c
1 parent 185a09b
commit 33d3c0c
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 9 deletions.
diff --git a/src/synthetic-homotopy-theory/shifts-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/shifts-sequential-diagrams.lagda.md
@@ -196,7 +196,7 @@ Given a cocone `c`
  X
 ```
 
-under `A`, we may forget the first injection and homotopy to get the cocone
+under `A`, we may forget the first inclusion and homotopy to get the cocone
 
 ```text
  a₁
@@ -320,10 +320,22 @@ module _
 
 ### Shifts of homotopies of cocones under sequential diagrams
 
-Given cocones `c` and `c'` under `A`, and a homotopy `H : c ~ c'` between them,
-which I'm not sufficiently artistically equipped to put into an ASCII diagram,
-we can again forget the first homotopy of maps and coherence to get the homotopy
-`H[1] : c[1] ~ c'[1]`. Inductively, we define `H[k + 1] ≐ H[k][1]`.
+Given cocones `c` and `c'` under `A`
+
+```text
+ a₀ a₁ a₀ a₁
+ A₀ ---> A₁ ---> A₂ ---> ⋯ A₀ ---> A₁ ---> A₂ ---> ⋯
+ \ | / \ | /
+ \ | i₁ / \ | i'₁ /
+ i₀ \ | / i₂ ~ i'₀ \ | / i'₂
+ \ | / \ | /
+ ∨ ∨ ∨ ∨ ∨ ∨
+ X X
+```
+
+and a homotopy `H : c ~ c'` between them, we can again forget the first homotopy
+of maps and coherence to get the homotopy `H[1] : c[1] ~ c'[1]`. Inductively, we
+define `H[k + 1] ≐ H[k][1]`.
 
 ```agda
 module _
@@ -363,9 +375,8 @@ module _
 
 ### Unshifts of homotopies of cocones under sequential diagrams
 
-Similarly to unshifting cocones, we can synthesize the first homotopy and
-coherence to unshift a homotopy of cocones. Given two cocones `c`, `c'` under
-`A[1]`
+Similarly to unshifting cocones, we can recover the first homotopy and coherence
+to unshift a homotopy of cocones. Given two cocones `c`, `c'` under `A[1]`
 
 ```text
  a₁ a₁

diff --git a/src/synthetic-homotopy-theory/total-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/total-sequential-diagrams.lagda.md
@@ -33,7 +33,8 @@ of a
 [dependent sequential diagram](synthetic-homotopy-theory.dependent-sequential-diagrams.md)
 `B : (A, a) → 𝒰` is the
 [sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md)
-consisting of [total spaces](foundation.dependent-pair-types.md) `Σ Aₙ Bₙ`.
+consisting of [total spaces](foundation.dependent-pair-types.md) `Σ Aₙ Bₙ` and
+total maps.
 
 ## Definitions