Sequential limits

src/foundation/cones-over-cospans.lagda.md

@@ -27,9 +27,9 @@ open import foundation-core.whiskering-homotopies
 
 ## Idea
 
-A **cone** on a [cospan](foundation.cospans.md) `A --f--> X <--g-- B` with
-domain `C` is a triple `(p,q,H)` consisting of a map `p : C → A`, a map
-`q : C → B`, and a homotopy `H` witnessing that the square
+A **cone on a [cospan](foundation.cospans.md)** `A -f-> X <-g- B` with domain
+`C` is a triple `(p, q, H)` consisting of a map `p : C → A`, a map `q : C → B`,
+and a homotopy `H` witnessing that the square
 
 ```text
       q

src/foundation/cones-over-towers.lagda.md

@@ -30,7 +30,7 @@ open import foundation-core.whiskering-homotopies
 
 ## Idea
 
-A **cone** over a [tower](foundation.towers.md) `A` with domain `X` is a
+A **cone over a [tower](foundation.towers.md) `A` with domain `X`** is a
 [sequence](foundation.dependent-sequences.md) of functions from `X` into the
 sequence of types of `A` such that the triangles
 

src/foundation/dependent-towers.lagda.md

@@ -77,7 +77,7 @@ pr2 (const-dependent-tower A B) n _ = map-tower B n
 
 ### Sections of a dependent tower
 
-A **section of a dependent tower** `(B , g)` over `(A , f)` is a choice of
+A **section of a dependent tower `(B , g)` over `(A , f)`** is a choice of
 sections `hₙ` of each `Bₙ` that vary naturally over `A`, by which we mean that
 the diagrams
 

src/foundation/equivalences-towers.lagda.md

@@ -34,9 +34,9 @@ An **equivalence of towers** `A ≃ B` is a commuting diagram of the form
 
 ```text
   ⋯ ----> Aₙ₊₁ ----> Aₙ ----> ⋯ ----> A₁ ----> A₀
-  |        |         |       |       |        |
+           |         |       |       |        |
   ⋯        |         |       ⋯       |        |
-  v        v         v       v       v        v
+           v         v       v       v        v
   ⋯ ----> Bₙ₊₁ ----> Bₙ ----> ⋯ ----> B₁ ----> B₀.
 ```
 

src/foundation/morphisms-towers.lagda.md

@@ -36,9 +36,9 @@ A **morphism of towers** `A → B` is a commuting diagram of the form
 
 ```text
   ⋯ ----> Aₙ₊₁ ----> Aₙ ----> ⋯ ----> A₁ ----> A₀
-  |        |         |       |       |        |
+           |         |       |       |        |
   ⋯        |         |       ⋯       |        |
-  v        v         v       v       v        v
+           v         v       v       v        v
   ⋯ ----> Bₙ₊₁ ----> Bₙ ----> ⋯ ----> B₁ ----> B₀.
 ```
 

src/foundation/towers.lagda.md

@@ -19,7 +19,7 @@ open import foundation.universe-levels
 
 ## Idea
 
-A **tower** of types `f` is a [sequence](foundation.sequences.md) of types
+A **tower of types** `f` is a [sequence](foundation.sequences.md) of types
 together with maps between every two consecutive types
 
 ```text