Some typos, wording improvements, and brief prose additions (#1186)

- Change namespace header wording from
   ```md
   ## Files in the ... folder
   ```
   to
   ```md
   ## Modules in the ... namespace
   ```
- Improve typesetting and wording in `foundation.telescopes`
- Add brief main module introduction to `modal-type-theory`
- Add a remark about polymorphism in module about the precategory of
posets
- A series of miscellaneous typo fixes

scripts/fix_imports.py

@@ -145,7 +145,7 @@ def prettify_imports_block(block):
 
             agdaBlockStart = utils.find_index(contents, '```agda')
             if len(agdaBlockStart) > 1:
-                print('Warning: No Agda import block found inside <details> block in:\n\t' +
+                print('Warning: No Agda import block found inside `<details>` block in:\n\t' +
                       str(fpath), file=sys.stderr)
                 status |= FLAG_NO_IMPORT_BLOCK
             continue

src/category-theory.lagda.md

@@ -8,7 +8,7 @@
 
 {{#include tables/precategories.md}}
 
-## Files in the category theory folder
+## Modules in the category theory namespace
 
 ```agda
 module category-theory where

src/commutative-algebra.lagda.md

@@ -1,6 +1,6 @@
 # Commutative algebra
 
-## Files in the commutative algebra folder
+## Modules in the commutative algebra namespace
 
 ```agda
 module commutative-algebra where

src/elementary-number-theory.lagda.md

@@ -1,6 +1,6 @@
 # Elementary number theory
 
-## Files in the elementary number theory folder
+## Modules in the elementary number theory namespace
 
 ```agda
 module elementary-number-theory where

src/finite-algebra.lagda.md

@@ -1,6 +1,6 @@
 # Finite algebra
 
-## Files in the finite algebra folder
+## Modules in the finite algebra namespace
 
 ```agda
 module finite-algebra where

src/finite-group-theory.lagda.md

@@ -1,6 +1,6 @@
 # Finite group theory
 
-## Files in the finite group theory folder
+## Modules in the finite group theory namespace
 
 ```agda
 module finite-group-theory where

src/foundation-core.lagda.md

@@ -1,6 +1,6 @@
 # Foundation core
 
-## Files in the foundation-core folder
+## Modules in the foundation-core namespace
 
 ```agda
 module foundation-core where

src/foundation.lagda.md

@@ -4,7 +4,7 @@
 {-# OPTIONS --guardedness #-}
 ```
 
-## Files in the foundation folder
+## Modules in the foundation namespace
 
 ```agda
 module foundation where

src/foundation/telescopes.lagda.md

@@ -16,35 +16,36 @@ open import foundation.universe-levels
 
 ## Idea
 
-A **telescope**, or **iterated type family**, is a list of type families
-`(A₀, A₁, A₂, ..., A_n)` consisting of
+A {{#concept "telescope" Disambiguation="of types" Agda=telescope}}, or
+**iterated type family**, is a list of type families `(A₀, A₁, A₂, …, Aₙ)`
+consisting of
 
 - a type `A₀`,
 - a type family `A₁ : A₀ → 𝒰`,
 - a type family `A₂ : (x₀ : A₀) → A₁ x₀ → 𝒰`,
-- ...
-- a type family `A_n : (x₀ : A₀) ... (x_(n-1) : A_(n-1) x₀ ... x_(n-2)) → 𝒰`.
+- ⋮
+- a type family `Aₙ : (x₀ : A₀) ⋯ (xₙ₋₁ : Aₙ₋₁ x₀ ⋯ xₙ₋₂) → 𝒰`.
 
-We say that a telescope `(A₀,...,A_n)` has **length** `n+1`. In other words, the
-length of the telescope `(A₀,...,A_n)` is the length of the (dependent) list
-`(A₀,...,A_n)`.
+We say that a telescope `(A₀, …, Aₙ)` has **length** `n+1`. In other words, the
+length of the telescope `(A₀, …, Aₙ)` is the length of the (dependent) list
+`(A₀, …, Aₙ)`.
 
 We encode the type of telescopes as a family of inductive types
 
 ```text
-  telescope : (l : Level) → ℕ → UUω
+  telescope : (l : Level) → ℕ → UUω.
 ```
 
 The type of telescopes is a [directed tree](trees.directed-trees.md)
 
 ```text
-  ... → T₃ → T₂ → T₁ → T₀,
+  ⋯ → T₃ → T₂ → T₁ → T₀,
 ```
 
-where `T_n` is the type of all telescopes of length `n`, and the map from
-`T_(n+1)` to `T_n` maps `(A₀,...,A_n)` to `(A₀,...,A_(n-1))`. The type of such
-directed trees can be defined as a coinductive record type, and we will define
-the tree `T` of telescopes as a particular element of this tree.
+where `Tₙ` is the type of all telescopes of length `n`, and the map from `Tₙ₊₁`
+to `Tₙ` maps `(A₀, …, Aₙ)` to `(A₀, …, Aₙ₋₁)`. The type of such directed trees
+can be defined as a coinductive record type, and we will define the tree `T` of
+telescopes as a particular element of this tree.
 
 ## Definitions
 
@@ -61,11 +62,7 @@ data
     (X → telescope l2 n) → telescope (l1 ⊔ l2) (succ-ℕ n)
 
 open telescope public
-```
-
-A very slight reformulation of `cons-telescope` for convenience:
 
-```agda
 prepend-telescope :
   {l1 l2 : Level} {n : ℕ} →
   (A : UU l1) → ({x : A} → telescope l2 n) → telescope (l1 ⊔ l2) (succ-ℕ n)
@@ -76,9 +73,9 @@ prepend-telescope A B = cons-telescope {X = A} (λ x → B {x})
 
 One issue with the previous definition of telescopes is that it is impossible to
 extract any type information from it. At the expense of giving up full universe
-polymorphism, we can define a notion of **telescopes at a universe level** that
-admits such projections. This definition is also compatible with the
-`--level-universe` restriction.
+polymorphism, we can define **telescopes at a universe level**. These admit such
+projections, and are moreover compatible with the `--level-universe`
+restriction.
 
 ```agda
 data telescope-Level (l : Level) : ℕ → UU (lsuc l)
@@ -114,17 +111,17 @@ apply-base-telescope P (cons-telescope A) =
 
 ### Telescopes as instance arguments
 
-To get Agda to infer telescopes, we help it along a little using
+To have Agda infer telescopes, we help it along using
 [instance arguments](https://agda.readthedocs.io/en/latest/language/instance-arguments.html).
-These are a special kind of implicit argument in Agda that are resolved by the
-instance resolution algorithm. We register building blocks for this algorithm to
-use below, i.e. _instances_. Then Agda will attempt to use those to construct
+These are a special kind of implicit argument that are resolved by _the instance
+resolution algorithm_. We register building blocks, called _instances_, for this
+algorithm to use below. Then Agda will attempt to use those to construct
 telescopes of the appropriate kind when asked to.
 
-In the case of telescopes, this has the unfortunate disadvantage that we can
-only define instances for fixed length telescopes. We have defined instances of
-telescopes up to length 18, so although Agda cannot infer a telescope of a
-general length using this approach, it can infer them up to this given length.
+In the case of telescopes, this has the disadvantage that we can only define
+instances for fixed length telescopes. We have defined instances of telescopes
+up to length 18, so although Agda cannot infer a telescope of a general length
+using this approach, it can infer them up to this given length.
 
 ```agda
 instance-telescope : {l : Level} {n : ℕ} → {{telescope l n}} → telescope l n
@@ -912,3 +909,7 @@ instance
 - [Dependent telescopes](foundation.dependent-telescopes.md)
 - [Iterated Σ-types](foundation.iterated-dependent-pair-types.md)
 - [Iterated Π-types](foundation.iterated-dependent-product-types.md)
+
+## External links
+
+- [type telescope](https://ncatlab.org/nlab/show/type+telescope) at $n$Lab

src/graph-theory.lagda.md

@@ -1,6 +1,6 @@
 # Graph theory
 
-## Files in the graph theory folder
+## Modules in the graph theory namespace
 
 ```agda
 module graph-theory where

src/group-theory.lagda.md

@@ -1,6 +1,6 @@
 # Group theory
 
-## Files in the group theory folder
+## Modules in the group theory namespace
 
 ```agda
 module group-theory where

src/higher-group-theory.lagda.md

@@ -1,6 +1,6 @@
 # Higher group theory
 
-## Files in the higher group theory folder
+## Modules in the higher group theory namespace
 
 ```agda
 module higher-group-theory where

src/linear-algebra.lagda.md

@@ -1,6 +1,6 @@
 # Linear algebra
 
-## Files in the linear algebra folder
+## Modules in the linear algebra namespace
 
 ```agda
 module linear-algebra where

src/lists.lagda.md

@@ -1,6 +1,6 @@
 # Lists
 
-## Files in the lists folder
+## Modules in the lists namespace
 
 ```agda
 module lists where

src/modal-type-theory.lagda.md

@@ -4,7 +4,20 @@
 {-# OPTIONS --cohesion --flat-split #-}
 ```
 
-## Files in the modal type theory folder
+Modal type theory is the study of type theory extended with syntactic _modal_
+operators. These are operations on types that increase the expressivity of the
+type theory in some way.
+
+In this namespace, we consider modal extensions of Martin-Löf type theory with a
+[flat modality](modal-type-theory.flat-modality.md) `♭`,
+[sharp modality](modal-type-theory.sharp-modality.md) `♯`, and more to come. The
+[adjoint pair of modalities](modal-type-theory.flat-sharp-adjunction.md)
+`♭ ⊣ ＃` display a structure on all types referred to as _spatial_, or
+_cohesive_ structure.
+
+- To read more, continue to [crisp types](modal-type-theory.crisp-types.md).
+
+## Modules in the modal type theory namespace
 
 ```agda
 module modal-type-theory where

src/modal-type-theory/action-on-homotopies-flat-modality.lagda.md

@@ -22,8 +22,9 @@ open import modal-type-theory.functoriality-flat-modality
 
 ## Idea
 
-Given a crisp [homotopy](foundation-core.homotopies.md) of maps `f ~ g`, then
-there is a homotopy `♭ f ~ ♭ g` where `♭ f` is the
+Given a [crisp](modal-type-theory.crisp-types.md)
+[homotopy](foundation-core.homotopies.md) of maps `f ~ g`, then there is a
+homotopy `♭ f ~ ♭ g` where `♭ f` is the
 [functorial action of the flat modality on maps](modal-type-theory.functoriality-flat-modality.md).
 
 ## Definitions

src/modal-type-theory/action-on-identifications-crisp-functions.lagda.md

@@ -20,12 +20,12 @@ open import modal-type-theory.crisp-identity-types
 
 ## Idea
 
-A function defined on [crisp elements](modal-type-theory.crisp-types.md)
-`f : @♭ A → B` preserves crisp
+A function defined on crisp elements `f : @♭ A → B` preserves crisp
 [identifications](foundation-core.identity-types.md), in the sense that it maps
 a crisp identification `p : x ＝ y` in `A` to an identification
 `crisp-ap f p : f x ＝ f y` in `B`. This action on identifications can be
-understood as crisp functoriality of crisp identity types.
+understood as crisp functoriality of [crisp](modal-type-theory.crisp-types.md)
+identity types.
 
 This is a strengthening of the
 [action on identifications of functions](foundation.action-on-identifications-functions.md)

src/modal-type-theory/action-on-identifications-flat-modality.lagda.md

@@ -22,8 +22,9 @@ open import modal-type-theory.flat-modality
 
 ## Idea
 
-Given a crisp [identification](foundation-core.identity-types.md) `x ＝ y` in
-`A`, then there is an identification `intro-flat x ＝ intro-flat y` in `♭ A`.
+Given a [crisp](modal-type-theory.crisp-types.md)
+[identification](foundation-core.identity-types.md) `x ＝ y` in `A`, then there
+is an identification `intro-flat x ＝ intro-flat y` in `♭ A`.
 
 ## Definitions
 

src/modal-type-theory/crisp-dependent-pair-types.lagda.md

@@ -99,7 +99,7 @@ module _
 
   compute-counit-flat-Σ :
     counit-flat {A = Σ A B} ~
-    ( map-Σ B counit-flat (λ where (intro-flat _) → counit-flat)) ∘
+    ( map-Σ B counit-flat counit-family-flat) ∘
     ( map-distributive-flat-Σ)
   compute-counit-flat-Σ (intro-flat _) = refl
 ```
@@ -117,7 +117,7 @@ module _
   is-flat-discrete-crisp-Σ is-disc-B =
     is-equiv-left-map-triangle
       ( counit-flat)
-      ( map-Σ B counit-flat (λ where (intro-flat _) → counit-flat))
+      ( map-Σ B counit-flat counit-family-flat)
       ( map-distributive-flat-Σ)
       ( λ where (intro-flat _) → refl)
       ( is-equiv-map-distributive-flat-Σ)
@@ -129,7 +129,7 @@ module _
     is-fiberwise-equiv-is-equiv-map-Σ
       ( B)
       ( counit-flat)
-      ( λ where (intro-flat _) → counit-flat)
+      ( counit-family-flat)
       ( is-disc-A)
       ( is-equiv-right-map-triangle
         ( counit-flat)

src/modal-type-theory/crisp-law-of-excluded-middle.lagda.md

@@ -22,7 +22,8 @@ open import foundation-core.propositions
 ## Idea
 
 The {{#concept "crisp law of excluded middle" Agda=Crisp-LEM}} asserts that any
-crisp [proposition](foundation-core.propositions.md) `P` is
+[crisp](modal-type-theory.crisp-types.md)
+[proposition](foundation-core.propositions.md) `P` is
 [decidable](foundation.decidable-types.md).
 
 ## Definition

src/modal-type-theory/crisp-types.lagda.md

@@ -44,13 +44,14 @@ one which is crisp and one which is cohesive, we may in a type signature write
 ```
 
 Observe that for us to be able to assume `x` is crisp at all, we must also
-assume that the type `A` and the universe level `l` are crisp, following the
-rule that crisp hypotheses may only be formed in crisp contexts.
-
-So what does it mean for `A` to be a {{#concept "crisp type"}}? Since the
-universe of types is itself a type, and every type comes equipped with cohesive
-structure, it means that the definition of `A` is indifferent to the cohesive
-structure on the universe.
+assume that the type `A` and the [universe level](foundation.universe-levels.md)
+`l` are crisp, following the rule that crisp hypotheses may only be formed in
+crisp contexts.
+
+So what does it mean for `A` to be a crisp type? Since the universe of types is
+itself a type, and every type comes equipped with cohesive structure, that `A`
+is a {{#concept "crisp type"}} means that the definition of `A` is indifferent
+to the cohesive structure on the universe.
 
 Note that saying a type is crisp is very different to saying that the cohesive
 structure of the type is trivial, which one could in one way informally state as

src/modal-type-theory/flat-discrete-crisp-types.lagda.md

@@ -36,8 +36,8 @@ open import modal-type-theory.functoriality-flat-modality
 
 ## Idea
 
-A crisp type is said to be
-{{$concept "flat discrete" Disambiguation="crisp type" Agda=is-flat-discrete-crisp}}
+A [crisp type](modal-type-theory.crisp-types.md) is said to be
+{{#concept "flat discrete" Disambiguation="crisp type" Agda=is-flat-discrete-crisp}}
 if it is [flat](modal-type-theory.flat-modality.md) modal. I.e. if the flat
 counit is an [equivalence](foundation-core.equivalences.md) at that type.
 
@@ -120,9 +120,9 @@ module _
 
   is-flat-discrete-crisp-equiv :
     @♭ A ≃ B → is-flat-discrete-crisp A → is-flat-discrete-crisp B
-  is-flat-discrete-crisp-equiv e bB =
+  is-flat-discrete-crisp-equiv e bA =
     is-equiv-htpy-equiv'
-      ( e ∘e (counit-flat , bB) ∘e action-flat-equiv (inv-equiv e))
+      ( e ∘e (counit-flat , bA) ∘e action-flat-equiv (inv-equiv e))
       ( λ where (intro-flat x) → is-section-map-inv-equiv e x)
 
   is-flat-discrete-crisp-equiv' :
@@ -133,7 +133,7 @@ module _
       ( λ where (intro-flat x) → is-retraction-map-inv-equiv e x)
 ```
 
-### Types `♭ A` are flat discrete
+### Types in the image of `♭` are flat discrete
 
 This is Theorem 6.18 of {{#cite Shu18}}.
 
@@ -152,15 +152,15 @@ Given crisp elements `x` and `y` of `A` We have a
 [commuting triangle](foundation-core.commuting-triangles-of-maps.md)
 
 ```text
-                               ♭ (x ＝ y)
-                                  ∧   |
-                     Eq-eq-flat /~    |
-                              /       |
-  (intro-flat x ＝ intro-flat y)      | counit-flat
-                              \       |
-               ap (counit-flat) \     |
-                                  ∨   ∨
-                                 (x ＝ y)
+                              ♭ (x = y)
+                                 ∧   |
+                     Eq-eq-flat /~   |
+                               /     |
+  (intro-flat x = intro-flat y)      | counit-flat
+                               \     |
+               ap (counit-flat) \    |
+                                 ∨   ∨
+                                (x = y)
 ```
 
 where the top-left map `Eq-eq-flat` is an equivalence. Thus, the right map is an