fix expressions in some headers

src/elementary-number-theory/addition-integers.lagda.md

@@ -424,7 +424,7 @@ is-binary-emb-add-ℤ =
   is-binary-emb-is-binary-equiv is-binary-equiv-left-add-ℤ
 ```
 
-### Addition by x is injective
+### Addition by `x` is injective
 
 ```agda
 is-injective-right-add-ℤ : (x : ℤ) → is-injective (_+ℤ x)

src/foundation-core/retractions.lagda.md

@@ -59,7 +59,7 @@ module _
 
 ## Properties
 
-### If A is a retraction of B, then the identity types of A are retractions of the identity types of B
+### If `A` is a retraction of `B`, then the identity types of `A` are retractions of the identity types of `B`
 
 ```agda
 module _

src/foundation-core/sets.lagda.md

@@ -77,7 +77,7 @@ module _
       ( contraction (is-proof-irrelevant-is-prop (H x x) refl) p)
 ```
 
-### If a reflexive binary relation maps into the identity type of A, then A is a set
+### If a reflexive binary relation maps into the identity type of `A`, then `A` is a set
 
 ```agda
 module _

src/foundation/equivalences-maybe.lagda.md

@@ -94,7 +94,7 @@ abstract
     is-not-exception-injective-map-exception-Maybe (is-injective-emb e)
 ```
 
-### If f is injective and f (inl x) is an exception, then f exception is a value
+### If `f` is injective and `f (inl x)` is an exception, then `f exception` is a value
 
 ```agda
 is-value-injective-map-exception-Maybe :

src/foundation/fiber-inclusions.lagda.md

@@ -62,7 +62,7 @@ module _
 
 ## Properties
 
-### The fiber inclusions are truncated maps for any type family B if and only if A is truncated
+### The fiber inclusions are truncated maps for any type family `B` if and only if `A` is truncated
 
 ```agda
 module _

src/foundation/unital-binary-operations.lagda.md

@@ -65,7 +65,7 @@ is-coherently-unital {A = A} μ = Σ A (coherent-unit-laws μ)
 
 ## Properties
 
-### The unit laws for an operation μ with unit e can be upgraded to coherent unit laws
+### The unit laws for an operation `μ` with unit `e` can be upgraded to coherent unit laws
 
 ```agda
 module _

src/group-theory/commutators-groups.lagda.md

@@ -38,7 +38,7 @@ module _
 
 ## Properties
 
-### The commutator of x and y is unit if and only x and y commutes
+### The commutator of `x` and `y` is unit if and only `x` and `y` commutes
 
 ```agda
 module _

src/lists/sorted-vectors.lagda.md

@@ -95,7 +95,7 @@ module _
   is-leq-head-head-tail-is-sorted-vec (x ∷ y ∷ v) s = pr1 s
 ```
 
-### If a vector `v' ＝ y ∷ v` is sorted then for all elements `x` less than or equal to `y`, `x` is less than or equal to every element in the vector.
+### If a vector `v' ＝ y ∷ v` is sorted then for all elements `x` less than or equal to `y`, `x` is less than or equal to every element in the vector
 
 ```agda
   is-least-element-vec-is-leq-head-sorted-vec :

src/trees/induction-w-types.lagda.md

@@ -78,7 +78,7 @@ module _
 
 ### Strong induction for W-types
 
-#### We define an operation □-𝕎 that acts on families over 𝕎 A B
+#### We define an operation `□-𝕎` that acts on families over `𝕎 A B`
 
 ```agda
 module _

src/univalent-combinatorics/counting-dependent-pair-types.lagda.md

@@ -118,7 +118,7 @@ abstract
   number-of-elements-count-Σ (pair k e) f = number-of-elements-count-Σ' k e f
 ```
 
-### If A and Σ A B can be counted, then each B x can be counted
+### If `A` and `Σ A B` can be counted, then each `B x` can be counted
 
 ```agda
 count-fiber-count-Σ :
@@ -137,7 +137,7 @@ count-fiber-count-Σ-count-base e f x =
   count-fiber-count-Σ (has-decidable-equality-count e) f x
 ```
 
-### If Σ A B and each B x can be counted, and if B has a section, then A can be counted
+### If `Σ A B` and each `B x` can be counted, and if `B` has a section, then `A` can be counted
 
 ```agda
 count-fib-map-section :

src/univalent-combinatorics/fibers-of-maps.lagda.md

@@ -42,7 +42,7 @@ The fibers of maps between finite types are finite.
 
 ## Properties
 
-### If A and B can be counted, then the fibers of a map f : A → B can be counted
+### If `A` and `B` can be counted, then the fibers of a map `f : A → B` can be counted
 
 ```agda
 count-fib :
@@ -134,7 +134,7 @@ is-decidable-fib-Fin {k} {l} f y =
   is-decidable-fib-count f (count-Fin k) (count-Fin l) y
 ```
 
-### If `f : A → B` and `B` is finite, then `A` is finite if and only if the fibers of f are finite
+### If `f : A → B` and `B` is finite, then `A` is finite if and only if the fibers of `f` are finite
 
 ```agda
 equiv-is-finite-domain-is-finite-fib :