chore: Fix some typos in the wild-category-theory module

src/universal-algebra.lagda.md

@@ -1,4 +1,4 @@
-# Universal Algebra
+# Universal algebra
 
 ## Files in the universal algebra folder
 

src/wild-category-theory/colax-functors-noncoherent-large-wild-higher-precategories.lagda.md

@@ -42,10 +42,8 @@ is an $(n+1)$-morphism
   Fₙ₊₁ (id-hom 𝒜 f) ⇒ id-hom ℬ (Fₙ f)
 ```
 
-in `ℬ`,
-
-and for every pair of composable $(n+1)$-morphisms `g` after `f` in `𝒜`, there
-is an $(n+2)$-morphism
+in `ℬ`, and for every pair of composable $(n+1)$-morphisms `g` after `f` in `𝒜`,
+there is an $(n+2)$-morphism
 
 ```text
   Fₙ₊₁ (g ∘ f) ⇒ (Fₙ₊₁ g) ∘ (Fₙ₊₁ f)

src/wild-category-theory/colax-functors-noncoherent-wild-higher-precategories.lagda.md

@@ -39,10 +39,8 @@ is an $(n+1)$-morphism
   Fₙ₊₁ (id-hom 𝒜 f) ⇒ id-hom ℬ (Fₙ f)
 ```
 
-in `ℬ`,
-
-and for every pair of composable $(n+1)$-morphisms `g` after `f` in `𝒜`, there
-is an $(n+2)$-morphism
+in `ℬ`, and for every pair of composable $(n+1)$-morphisms `g` after `f` in `𝒜`,
+there is an $(n+2)$-morphism
 
 ```text
   Fₙ₊₁ (g ∘ f) ⇒ (Fₙ₊₁ g) ∘ (Fₙ₊₁ f)

src/wild-category-theory/isomorphisms-in-noncoherent-large-wild-higher-precategories.lagda.md

@@ -22,9 +22,9 @@ open import wild-category-theory.noncoherent-large-wild-higher-precategories
 
 Consider a
 [noncoherent large wild higher precategory](wild-category-theory.noncoherent-large-wild-higher-precategories.md)
-𝒞. An
+`𝒞`. An
 {{#concept "isomorphism" Disambiguation="in noncoherent large wild higher precategories" Agda=is-iso-Noncoherent-Large-Wild-Higher-Precategory}}
-in 𝒞 is a morphism `f : x → y` in 𝒞 [equipped](foundation.structure.md) with
+in `𝒞` is a morphism `f : x → y` in `𝒞` [equipped](foundation.structure.md) with
 
 - a morphism `s : y → x`
 - a $2$-morphism `is-split-epi : f ∘ s → id`, where `∘` and `id` denote

src/wild-category-theory/isomorphisms-in-noncoherent-wild-higher-precategories.lagda.md

@@ -21,9 +21,9 @@ open import wild-category-theory.noncoherent-wild-higher-precategories
 
 Consider a
 [noncoherent wild higher precategory](wild-category-theory.noncoherent-wild-higher-precategories.md)
-𝒞. An
+`𝒞`. An
 {{#concept "isomorphism" Disambiguation="in noncoherent wild higher precategories" Agda=is-iso-Noncoherent-Wild-Higher-Precategory}}
-in 𝒞 is a morphism `f : x → y` in 𝒞 [equipped](foundation.structure.md) with
+in `𝒞` is a morphism `f : x → y` in `𝒞` [equipped](foundation.structure.md) with
 
 - a morphism `s : y → x`
 - a $2$-morphism `is-split-epi : f ∘ s → id`, where `∘` and `id` denote

src/wild-category-theory/noncoherent-large-wild-higher-precategories.lagda.md

@@ -32,7 +32,7 @@ open import wild-category-theory.noncoherent-wild-higher-precategories
 
 ## Idea
 
-It is a important open problem known as the _coherence problem_ to define a
+It is an important open problem known as the _coherence problem_ to define a
 fully coherent notion of $∞$-category in univalent type theory. The subject of
 _wild category theory_ attempts to recover some of the benefits of $∞$-category
 theory without tackling this problem. We introduce, as one of our basic building

src/wild-category-theory/noncoherent-wild-higher-precategories.lagda.md

@@ -30,16 +30,16 @@ open import structured-types.transitive-globular-types
 
 ## Idea
 
-It is a important open problem known as the _coherence problem_ to define a
+It is an important open problem known as the _coherence problem_ to define a
 fully coherent notion of $∞$-category in univalent type theory. The subject of
 _wild category theory_ attempts to recover some of the benefits of $∞$-category
 theory without tackling this problem. We introduce, as one of our basic building
 blocks in this subject, the notion of a _noncoherent wild higher precategory_.
 
 A _noncoherent wild higher precategory_ `𝒞` is a structure that attempts at
-capturing the structure of an higher precategory to the $0$'th order. It
-consists of in some sense all of the operations and none of the coherence of an
-higher precategory. Thus, it is defined as a
+capturing the structure of a higher precategory to the $0$'th order. It consists
+of in some sense all of the operations and none of the coherence of a higher
+precategory. Thus, it is defined as a
 [globular type](structured-types.globular-types.md) with families of
 $n$-morphisms labeled as "identities"