Skip to content

Commit

Permalink
prose: fix typos, improve wording.
Browse files Browse the repository at this point in the history
  • Loading branch information
TOTBWF committed Aug 9, 2024
1 parent 37b5b9e commit 5becc68
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 4 deletions.
1 change: 1 addition & 0 deletions src/Borceux.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -895,6 +895,7 @@ _ = Path-category
_ = Free-category
_ = Comm-graph
_ = Comm-graphs
_ = Comm-free-category
```
-->

Expand Down
8 changes: 4 additions & 4 deletions src/Cat/Instances/CommGraphs.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -227,7 +227,7 @@ Strict-cats↪Comm-graphs-full
To see why, suppose that $f : \cC \to \cD$ is a commutative
graph homomorphism between strict categories. By definition, $f$
already contains the data of a functor; the tricky part is showing
the properties.
that this data is functorial.

```agda
Strict-cats↪Comm-graphs-full {x = C} {y = D} f =
Expand All @@ -244,7 +244,7 @@ Strict-cats↪Comm-graphs-full {x = C} {y = D} f =
The trick is that commutative graph homomorphisms between categories cannot observe
the intensional structure of paths, as they must preserve all commutativities.
In particular, $f$ will preserve the commutativity in $\cC$ between the singleton path
containing $id$ is equal to the empty path; so $f(\id) = \id$
$[id]$ and the empty path; so $f(\id) = \id$

```agda
functor .F-id =
Expand All @@ -254,7 +254,7 @@ containing $id$ is equal to the empty path; so $f(\id) = \id$
```

Additionally, $f$ will preserve the commutativity between the singleton
path $g \circ h$ and the path $h, g$, so $f(g \circ h) = f g \circ f h$.
path $[g \circ h]$ and the path $[h, g]$, so $f(g \circ h) = f g \circ f h$.

```agda
functor .F-∘ g h =
Expand Down Expand Up @@ -363,7 +363,7 @@ module _ (C : Σ (Precategory o ℓ) is-strict) where
path-fold C (f .hom) p ≡ path-fold C (f .hom) q
```

The proof is an easy but tedious application of the elimination principe
The proof is an easy but tedious application of the elimination principle
of `Commutative`{.Agda}.

```agda
Expand Down

0 comments on commit 5becc68

Please sign in to comment.