chore: fix typos

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.
 

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/Monad/Extension.lagda.md

@@ -39,7 +39,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/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/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/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/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

src/Cat/Regular/Slice.lagda.md

@@ -85,7 +85,7 @@ finitely complete, and instead characterise the _extremal_ epimorphisms.
 [strong epimorphisms]: Cat.Morphism.Strong.Epi.html
 
 For this, it will suffice to show that the inclusion functor $\cC/y
-\mono \cC$ both preserves and reflects extermal epimorphisms. Given an
+\mono \cC$ both preserves and reflects extremal epimorphisms. Given an
 extremal epi $h : a \epi b$ over $y$, and a non-trivial factorisation of
 $h$ through a monomorphism $m$ in $\cC$, we can show that $m$ itself is
 a monomorphism $bm \to b$ over $y$, and that it factors $h$ in $\cC/y$.

src/Data/Bool.lagda.md

@@ -27,7 +27,7 @@ module Data.Bool where
 open import Data.Bool.Base public
 ```
 
-Pattern matching on only the first argument might seem like a somewhat inpractical choice
+Pattern matching on only the first argument might seem like a somewhat impractical choice
 due to its asymmetry - however, it shortens a lot of proofs since we get a lot of judgemental
 equalities for free. For example, see the following statements:
 

src/Data/Set/Projective.lagda.md

@@ -219,7 +219,7 @@ every proposition is set-projective if and only if every set has split support.
 The following proof is adapted from [@Kraus-Escardó-Coquand-Altenkirch:2016].
 
 We will start with the reverse direction. Suppose that every proposition
-is set projective, and let $A$ be a set. The truncation of $A$ is a propositon,
+is set projective, and let $A$ be a set. The truncation of $A$ is a propositton,
 and the constant family $\| A \| \to A$ is a set-indexed family, so projectivity
 of $\| A \|$ directly gives us split support.
 

src/Homotopy/Pushout.lagda.md

@@ -82,7 +82,7 @@ for the function projecting into `⊤`{.Agda} - `const tt`{.Agda}.
 
 If one considers the structure we're creating, it becomes very
 obvious that this is equivalent to suspension - because both of our
-non-path constructors have input `⊤`{.Agda}, they're indistiguishable
+non-path constructors have input `⊤`{.Agda}, they're indistinguishable
 from members of the pushout; therefore, we take the
 `inl`{.Agda} and `inr`{.Agda} to `N`{.Agda} and
 `S`{.Agda} respectively.
@@ -116,7 +116,7 @@ similarities in structure.</summary>
   open is-iso
 
   iso-pf : is-iso Susp→Pushout-⊤←A→⊤
-  iso-pf .inv = Pushout-⊤←A→⊤-to-Susp 
+  iso-pf .inv = Pushout-⊤←A→⊤-to-Susp
   iso-pf .rinv (inl x) = refl
   iso-pf .rinv (inr x) = refl
   iso-pf .rinv (commutes c i) = refl
@@ -191,7 +191,7 @@ and again mostly reduces to `refl`{.Agda}.
                      (λ x → t (inr x)) ,
                      (λ c i → ap t (commutes c) i)
 
-  Cocone→Pushout t (inl x) = fst t x 
+  Cocone→Pushout t (inl x) = fst t x
   Cocone→Pushout t (inr x) = fst (snd t) x
   Cocone→Pushout t (commutes c i) = snd (snd t) c i
 

src/Logic/Propositional/Classical.lagda.md

@@ -505,7 +505,7 @@ opaque
 -->
 
 We also define a notion of semantic entailment, wherein `ψ` semantically
-entails `P` when for every assigment of variables `ρ`, if `⟦ ψ ⟧ ρ ≡
+entails `P` when for every assignment of variables `ρ`, if `⟦ ψ ⟧ ρ ≡
 true`, then `⟦ P ⟧ ρ ≡ true`.
 
 ```agda

src/Order/DCPO/Pointed.lagda.md

@@ -190,7 +190,7 @@ This follows from som quick induction.
     least-fix y p = ⋃.least _ _ _ (fⁿ⊥≤fix y p)
 ```
 
-Now, let's show that $\bigcup (f^{n}(\bot))$ is actuall a fixpoint.
+Now, let's show that $\bigcup (f^{n}(\bot))$ is actually a fixpoint.
 First, the forward direction: $\bigcup (f^{n}(\bot)) \le f (\bigcup (f^{n}(\bot)))$.
 This follows directly from Scott-continuity of $f$.
 

src/index.lagda.md

@@ -466,7 +466,7 @@ open import Cat.Displayed.Instances.Externalisation
 
 ## Order theory
 
-The study of sets equipped with a notion of precendence, or containment;
+The study of sets equipped with a notion of precedence, or containment;
 while the theory of [[partial orders]] is naturally seen as a
 restriction of the theory of categories, formalising these concepts
 separately leads to cleaner mathematics.