chore: gardening

CONTRIBUTING.md

@@ -234,7 +234,7 @@ common name, that **can** be used instead of deriving a name based on
 its type.
 
 Sometimes, this can result in verbose names. A bit of verbosity is
-preferrable to having a theorem whose name is not memorable. Deciding on
+preferable to having a theorem whose name is not memorable. Deciding on
 a good name for your lemma can be very hard: don't hesitate to ask on
 Discord for help.
 

_typos.toml

@@ -0,0 +1,31 @@
+[files]
+extend-exclude = ["support", "*.scss", "*.bibtex"]
+
+[default.extend-words]
+identicals = "identicals"
+intensional = "intensional"
+operad = "operad"
+projectives = "projectives"
+raison = "raison"
+substituters = "substituters"
+
+# parts of identifiers
+ba = "ba"
+cancell = "cancell"
+DNE = "DNE"
+fo = "fo"
+Iy = "Iy"
+hom = "hom"
+lits = "lits"
+ment = "ment"
+mor = "mor"
+nam = "nam"
+nto = "nto"
+padd = "padd"
+pn = "pn"
+Singl = "Singl"
+SinglP = "SinglP"
+som = "som"
+toi = "toi"
+ue = "ue"
+unitl = "unitl"

src/1Lab/Reflection/Copattern.agda

@@ -141,7 +141,7 @@ define-copattern nm {A = A} x = do
   make-copattern false nm `x `A
 
 {-
-There is a slight caveat with level-polymorphic defintions, as
+There is a slight caveat with level-polymorphic definitions, as
 they cannot be quoted into any `Type ℓ`. With this in mind,
 we also provide a pair of macros that work over `Typeω` instead.
 -}

src/Cat/Allegory/Base.lagda.md

@@ -201,7 +201,7 @@ Relational composition is again given by the familiar formula: The
 composite of $R$ and $S$ is given by the relation which "bridges the
 gap", i.e. $(R \circ S)(x, z)$ iff. there exists some $y$ such that
 $R(x, y)$ and $S(y, z)$. I'm not sure how surprising this will be to
-some of you --- embarassingly, it was fairly surprising to me --- but
+some of you --- embarrassingly, it was fairly surprising to me --- but
 the identity relation is.. the identity relation:
 
 ```agda

src/Cat/Diagram/Initial.lagda.md

@@ -122,7 +122,7 @@ Strictness is a property of, not structure on, an initial object.
 ```
 
 As maps out of initial objects are unique, it suffices to show that
-every map $\text{!`} \circ f = id$ for every $f : X \to \bot$ to establish that $\bot$ is a
+every map $\text{!`} \circ f = \id$ for every $f : X \to \bot$ to establish that $\bot$ is a
 strict initial object.
 
 ```agda

src/Cat/Diagram/Limit/Base.lagda.md

@@ -103,7 +103,7 @@ Natural transformations! Concretely, let $D : \cJ \to \cC$ be some
 diagram.  We can encode the same data as a cone in a natural
 transformation $\eps : {!x} \circ \mathord{!} \to D$, where $!x : \top
 \to \cC$ denotes the constant functor that maps object to $x$ and every
-morphism to $id$, and $! : \cJ \to \top$ denotes the unique functor into
+morphism to $\id$, and $! : \cJ \to \top$ denotes the unique functor into
 the [[terminal category]]. The components of such a natural
 transformation yield maps from $x \to D(j)$ for every $j : \cJ$, and
 naturality ensures that these maps must commute with the rest of the

src/Cat/Diagram/Monad/Extension.lagda.md

@@ -40,7 +40,7 @@ that characterises a monad. This has a couple of immediate benefits:
 
 3. It is not immediately clear how to generalize monads beyond
    endofunctors.
-   In constrast, extension systems can be readily generalized to
+   In contrast, extension systems can be readily generalized to
    [[relative extension systems]]^[In fact, we will *define* extension
    systems as a special case of relative extension systems!].
 

src/Cat/Diagram/Projective.lagda.md

@@ -156,7 +156,7 @@ preserves-epis→projective {P = P} hom-epi {X = X} {Y = Y} p e =
     p
 ```
 
-For the reverse direciton, let $P$ be projective, $f : X \epi Y$ be an epi,
+For the reverse direction, let $P$ be projective, $f : X \epi Y$ be an epi,
 and $g, h : \cC(P, X) \to A$ be a pair of functions into an arbitrary
 set $A$ such that $g(f \circ s) = h(f \circ s)$ for any $s : \cC(P, X)$.
 To show that $\cC(P,-)$ preserves epis, we must show that $g = h$, which

src/Cat/Diagram/Separator.lagda.md

@@ -351,7 +351,7 @@ $$g \circ e_i \circ r_i \circ f_i = h \circ e_i \circ r_i \circ f_i$$
 
 by our hypothesis. Finally, we can use the fact that $f_i$ and $r_i$
 are a section/retraction pair to observe that $g \circ e_i = f \circ e_i$,
-completeing the proof
+completing the proof
 
 ```agda
 retracts+separating-family→separator

src/Cat/Displayed/Bifibration.lagda.md

@@ -213,7 +213,7 @@ equivalence.
 ```
 
 <details>
-<summary>Futhermore, this equivalence is natural, but that's a very tedious proof.
+<summary>Furthermore, this equivalence is natural, but that's a very tedious proof.
 </summary>
 
 ```agda

src/Cat/Displayed/Cartesian/Right.lagda.md

@@ -82,7 +82,7 @@ To see this, recall that [[cartesian morphisms]] are [stable under
 vertical retractions]. The cartesian lift $f^{*}$ of $f$ is obviously
 cartesian, so it suffices to show that there is a vertical retraction
 $x^{*} \to x'$. To construct this retraction, we shall factorize $f'$
-over $f \cdot id$; which yields a vertical morphism $i^{*} : x' \to x^{*}$.
+over $f \cdot \id$; which yields a vertical morphism $i^{*} : x' \to x^{*}$.
 By our hypotheses, $i^{*}$ is invertible, and thus is a retraction.
 What remains to be shown is that the inverse to $i^{*}$ factors
 $f'$ and $f^{*}$; this follows from the factorisation of $f'$ and

src/Cat/Displayed/Cartesian/Weak.lagda.md

@@ -462,9 +462,9 @@ weak-fibration→weak-cartesian-factors {y' = y'} {f = f} wfib f' = weak-factor
 ## Weak fibrations and equivalence of Hom sets
 
 If $\cE$ is a weak fibration, then the hom sets $x' \to_f y'$ and
-$x' \to_{id} f^{*}(y')$ are equivalent, where $f^{*}(y')$ is the domain
+$x' \to_{\id} f^{*}(y')$ are equivalent, where $f^{*}(y')$ is the domain
 of the lift of $f$ along $y'$. To go from $f' : x' \to_u y'$ to
-$x' \to_{id} f^{*}(y')$, we use the vertical component of the
+$x' \to_{\id} f^{*}(y')$, we use the vertical component of the
 factorisation of $f'$; this forms an equivalence, as this factorisation
 is unique.
 
@@ -566,7 +566,7 @@ natural.
 
 We then proceed to construct a weak lift of $f$. We can use our object
 lifting function to construct the domain of the lift, apply the inverse
-direction of the equivalence to $id' : f^{*}(y') \to f^{*}(y')$ to
+direction of the equivalence to $\id' : f^{*}(y') \to f^{*}(y')$ to
 obtain the required lifting $x' \to_{f} f^{*}(y')$.
 
 ```agda
@@ -675,7 +675,7 @@ module _ (fib : Cartesian-fibration) where
 -->
 
 If we combine this with `weak-fibration→hom-iso-into`{.Agda}, we obtain
-a natural iso between $\cE_{u}(-,-)$ and $\cE_{id}(-,u^{*}(-))$.
+a natural iso between $\cE_{u}(-,-)$ and $\cE_{\id}(-,u^{*}(-))$.
 
 ```agda
   fibration→hom-iso

src/Cat/Displayed/Cocartesian/Weak.lagda.md

@@ -355,7 +355,7 @@ in the following diagram commutes.
 As a general fact, every morphism in a cartesian fibration factors into
 a composite of a cartesian and vertical morphism, obtained by taking
 the universal factorisation of $m' : y' \to{m \cdot i} u'$. We shall
-denote this morphism as $id*$.
+denote this morphism as $\id^*$.
 
 ~~~{.quiver}
 \begin{tikzcd}
@@ -374,7 +374,7 @@ denote this morphism as $id*$.
   \arrow["{m^{*}}", from=1-3, to=1-5]
   \arrow["{h^{*}}", from=2-1, to=1-3]
   \arrow["{h^{**}}", curve={height=-6pt}, from=2-3, to=1-3]
-  \arrow["{id^{*}}"', color={rgb,255:red,214;green,92;blue,92}, curve={height=6pt}, from=2-3, to=1-3]
+  \arrow["{\id^{*}}"', color={rgb,255:red,214;green,92;blue,92}, curve={height=6pt}, from=2-3, to=1-3]
 \end{tikzcd}
 ~~~
 
@@ -399,13 +399,13 @@ blue commutes.
   \arrow["{m^{*}}", from=1-3, to=1-5]
   \arrow["{h^{*}}", color={rgb,255:red,92;green,92;blue,214}, from=2-1, to=1-3]
   \arrow["{h^{**}}", curve={height=-6pt}, from=2-3, to=1-3]
-  \arrow["{id^{*}}"', color={rgb,255:red,92;green,92;blue,214}, curve={height=6pt}, from=2-3, to=1-3]
+  \arrow["{\id^{*}}"', color={rgb,255:red,92;green,92;blue,214}, curve={height=6pt}, from=2-3, to=1-3]
 \end{tikzcd}
 ~~~
 
 $h^{*}$ is the unique vertical map that factorises $h'$ through $m'$,
 and $h' = m' \cdot f'$ by our hypothesis, so it suffices to show that
-$m^{*} \cdot id^{*} \cdot f' = m' \cdot f'$. This commutes because
+$m^{*} \cdot \id^{*} \cdot f' = m' \cdot f'$. This commutes because
 $m^{*}$ is cartesian, thus finishing the proof.
 
 ```agda
@@ -614,7 +614,7 @@ cartesian+weak-opfibration→opfibration fib wlifts =
 # Weak opfibrations and equivalence of Hom sets
 
 If $\cE$ is a weak opfibration, then the hom sets $x' \to_f y'$ and
-$f^{*}(x') \to_{id} y'$ are equivalent, where $f^{*}(x')$ is the codomain
+$f^{*}(x') \to_{\id} y'$ are equivalent, where $f^{*}(x')$ is the codomain
 of the lift of $f$ along $y'$.
 
 ```agda

src/Cat/Displayed/Instances/Chaotic.lagda.md

@@ -79,7 +79,7 @@ is-iso→chaotic-cartesian {f = f} {g = g} is-inv = cart
       inv J.∘ h             ∎
 ```
 
-This implies that the chaotic fibration is a fibration, as $id$ is
+This implies that the chaotic fibration is a fibration, as $\id$ is
 invertible, and also lies above every morphism in $\cB$. We could
 use our lemmas from before to show this, but doing it by hand lets
 us avoid an extra `id` composite when constructing the universal map.

src/Cat/Displayed/Instances/Externalisation.lagda.md

@@ -255,7 +255,7 @@ Externalisation-fibration u y = u-lift where
 
 The externalisation is always globally small. We shall use the object of
 objects $C_0$ as the base for our generic object, and the identity
-morphism $id : C_0 \to C_0$ as the upstairs portion. Classifying maps
+morphism $\id : C_0 \to C_0$ as the upstairs portion. Classifying maps
 in the base are given by interpreting using a object $\cC(\Gamma, C_0)$ in
 the externalisation as a morphism in the base, and the displayed
 classifying map is the internal identity morphism, which is always

src/Cat/Displayed/Instances/Family.lagda.md

@@ -441,8 +441,8 @@ Family-gaunt-generic-object→Gaunt ob-set gaunt-gobj =
 
 To see that all automorphisms of $\cC$ are trivial, note that any automorphism
 $f : x \cong x$ induces a cartesian morphism $\{ x \} \to Ob$. Furthermore, this
-cartesian morphism must be unique, as $Ob$ is a gaunt generic object. However, $id$
-also yields a cartesian morphism $\{ x \} \to Ob$, so $f = id$.
+cartesian morphism must be unique, as $Ob$ is a gaunt generic object. However, $\id$
+also yields a cartesian morphism $\{ x \} \to Ob$, so $f = \id$.
 
 ```agda
   trivial-automorphism : ∀ {x} → (f : x ≅ x) → f ≡ id-iso

src/Cat/Displayed/Instances/Simple.lagda.md

@@ -41,7 +41,7 @@ structure to study simply-typed languages that have enough structure
 to represent contexts internally (i.e.: product types).
 
 To start, we fix some base category $\cB$ with binary products.
-Intuitvely, this will be some sort of category of contexts, and
+Intuitively, this will be some sort of category of contexts, and
 context extension endows this category with products. We interpret a
 type in a context to be an object $\Gamma \times X : \cB$.
 
@@ -62,7 +62,7 @@ situation (IE: STLC without products), then we need to consider a more
 For the maps, we already have the map $\Gamma \to \Delta$ as the
 base morphism, so the displayed portion of the map will be the
 map $\Gamma \times X \to Y$ between derivations. The identity
-morphism $id : \Gamma \times Y \to Y$ ignores the context, and
+morphism $\id : \Gamma \times Y \to Y$ ignores the context, and
 derives $Y$ by using the $Y$ we already had, and is thus represented
 by the second projection $\pi_2$.
 

src/Cat/Displayed/Path.lagda.md

@@ -250,7 +250,7 @@ $x$, giving a line of type families `p1`{.Agda} ranging from $\cE[-]
 
 We now "just" have to produce inhabitants of `p2`{.Agda} along $i : \II$
 which restrict to $\cE$ and $\cF$'s identity morphisms (and
-composition morphisms) at the endoints of $i$. We can do so by gluing,
+composition morphisms) at the endpoints of $i$. We can do so by gluing,
 now at the level of terms, against a heterogeneous composition. The
 details are quite nasty, but the core of it is extending the witness
 that $G$ respects identity to a path, over line given by gluing

src/Cat/Functor/Adjoint/Kan.lagda.md

@@ -136,7 +136,7 @@ cell $\sigma' : G \to RM$, and let $\sigma : LG \to M$ be its adjunct.
             module RM = Functor (R F∘ M)
 ```
 
-And since every part of the process in the preceeding paragraph is an
+And since every part of the process in the preceding paragraph is an
 isomorphism, this is indeed a factorisation, and it's unique to boot:
 we've shown that $LG$ is the extension of $LF$ along $p$!
 

src/Cat/Functor/Adjoint/Properties.lagda.md

@@ -178,7 +178,7 @@ $$
 \eta \circ s \circ R(f) \circ \eta = R(f) \circ \eta
 $$
 
-Finally, $\eta \circ s = id$, as $s$ is a section.
+Finally, $\eta \circ s = \id$, as $s$ is a section.
 
 ```agda
   unit-split-epic→left-full

src/Cat/Functor/Properties.lagda.md

@@ -27,7 +27,7 @@ open Functor
 
 # Functors
 
-This module defines the most important clases of functors: Full,
+This module defines the most important classes of functors: full,
 faithful, fully faithful (abbreviated ff), _split_ essentially
 surjective and ("_merely_") essentially surjective.
 

src/Cat/Instances/Free.lagda.md

@@ -310,7 +310,7 @@ open Graph
 -->
 
 Let $G$ be a graph, $\cC$ a strict category, and $f : G \to \cC$
-a [[graph homomorphism]] between $G$ and the underying graph of
+a [[graph homomorphism]] between $G$ and the underlying graph of
 $\cC$. We can extend $f$ to a function $fold(f)$ from paths in $G$ to morphisms
 in $\cC$ via induction.
 
@@ -418,7 +418,7 @@ the innocent reader.
 ```
 </details>
 
-With these lemmas out of the way, we can return to our orginal goal.
+With these lemmas out of the way, we can return to our original goal.
 The unit of the free object is given by the graph homomorphism that
 takes an edge to a singleton path, the universal morphism is given
 by our functor `PathF`{.Agda} from earlier, and the universal property

src/Cat/Instances/Localisation.lagda.md

@@ -275,7 +275,7 @@ module _ {o ℓ w} (C : Precategory o ℓ) (W : Wide-subcat C w) where
 We thus have the localisation as a [[precategory]]. The localisation
 functor $\cL : \cC \to \cC\loc{W}$ sends a morphism $f : a \to b$ to the
 singleton zigzag consisting of $f$ pointing forwards. Finally, if $f \in
-W$, then we're also allowed to draw it backards; and this inverts $\cL
+W$, then we're also allowed to draw it backwards; and this inverts $\cL
 f$. Since we're just writing down things we've already shown, there's a
 bit of code with not much more we could say:
 

src/Cat/Instances/MarkedGraphs.lagda.md

@@ -282,7 +282,7 @@ module _ (G : Marked-graph o ℓ) where
 -->
 
 In this section, we will detail how to freely construct a category
-from a marked graph $G$. Intuitvely, this works by freely generating
+from a marked graph $G$. Intuitively, this works by freely generating
 a category from $G$, and then identifying all marked pairs.
 However, there is a slight subtlety here: the marked pairs of $G$
 may not respect path concatenation, and may not even form an equivalence

src/Cat/Instances/Shape/Terminal.lagda.md

@@ -40,7 +40,7 @@ trivial morphisms.
 ⊤Cat .assoc _ _ _ _ = tt
 ```
 
-The ony morphism in the terminal category is the identity, so the
+The only morphism in the terminal category is the identity, so the
 terminal category is a [[pregroupoid]].
 
 ```agda

src/Cat/Internal/Base.lagda.md

@@ -49,8 +49,8 @@ _object of composable pairs_.
   {C_1} && {C_0}
   \arrow[from=1-1, to=1-3]
   \arrow[from=1-1, to=3-1]
-  \arrow["tgt", from=1-3, to=3-3]
-  \arrow["src"', from=3-1, to=3-3]
+  \arrow["\tgt", from=1-3, to=3-3]
+  \arrow["\src"', from=3-1, to=3-3]
   \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-3]
 \end{tikzcd}
 ~~~
@@ -66,7 +66,7 @@ constraints.
   \\
   \\
   {C_1 \times_{C_0} C_1} &&& {C_1}
-  \arrow["{id \times c}"', from=1-1, to=4-1]
+  \arrow["{\id \times c}"', from=1-1, to=4-1]
   \arrow["c"', from=4-1, to=4-4]
   \arrow["{\langle c \circ \langle \pi_1, \pi_1 \circ \pi_2 \rangle , \pi_2 \circ \pi_2\rangle}", from=1-1, to=1-4]
   \arrow["c", from=1-4, to=4-4]
@@ -115,11 +115,11 @@ making the following diagram commute.
   \\
   & {C_1} \\
   {C_0} && {C_0}
-  \arrow["hom"{description}, from=1-2, to=3-2]
+  \arrow["\mathrm{hom}"{description}, from=1-2, to=3-2]
   \arrow["x"', curve={height=6pt}, from=1-2, to=4-1]
   \arrow["y", curve={height=-6pt}, from=1-2, to=4-3]
-  \arrow["src"{description}, from=3-2, to=4-1]
-  \arrow["tgt"{description}, from=3-2, to=4-3]
+  \arrow["\src"{description}, from=3-2, to=4-1]
+  \arrow["\tgt"{description}, from=3-2, to=4-3]
 \end{tikzcd}
 ~~~
 

src/Cat/Internal/Functor/Outer.lagda.md

@@ -71,7 +71,7 @@ of $\bC$.
 
 The next data captures how $\bC$'s morphisms act on the fibres. Since
 the family-fibration correspondence takes dependency to sectioning, we
-require an assigment sending maps $f : P_0(x) \to y$ to maps $P_1(f) :
+require an assignment sending maps $f : P_0(x) \to y$ to maps $P_1(f) :
 \Gamma \to P$, which satisfy $y = P_0(P_1(f))$.
 
 ```agda

src/Cat/Morphism.lagda.md

@@ -178,7 +178,7 @@ subst-is-epic f=g f-epic h i p =
 ## Sections {defines=section}
 
 A morphism $s : B \to A$ is a section of another morphism $r : A \to B$
-when $r \cdot s = id$. The intuition for this name is that $s$ picks
+when $r \cdot s = \id$. The intuition for this name is that $s$ picks
 out a cross-section of $a$ from $b$. For instance, $r$ could map
 animals to their species; a section of this map would have to pick out
 a canonical representative of each species from the set of all animals.
@@ -272,7 +272,7 @@ subst-section p s .is-section = ap₂ _∘_ (sym p) refl ∙ s .is-section
 ## Retracts {defines="retract"}
 
 A morphism $r : A \to B$ is a retract of another morphism $s : B \to A$
-when $r \cdot s = id$. Note that this is the same equation involved
+when $r \cdot s = \id$. Note that this is the same equation involved
 in the definition of a section; retracts and sections always come in
 pairs. If sections solve a sort of "curation problem" where we are
 asked to pick out canonical representatives, then retracts solve a

src/Cat/Morphism/Orthogonal.lagda.md

@@ -188,7 +188,7 @@ type of lifts of such a square is a proposition.
 ```
 
 Dually, if $g$ is a [[monomorphism]], then we the type of lifts is also
-a propostion.
+a proposition.
 
 ```agda
   right-monic→lift-is-prop