Skip to content

Commit

Permalink
chore: fixup macro spacing (#199)
Browse files Browse the repository at this point in the history
fixes the stupid macro spacing that i introduced in #182
  • Loading branch information
plt-amy authored Mar 14, 2023
1 parent 21c176a commit 26bdece
Show file tree
Hide file tree
Showing 7 changed files with 12 additions and 12 deletions.
2 changes: 1 addition & 1 deletion src/Cat/Abelian/Base.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -140,7 +140,7 @@ $-ab = (-a)b = a(-b)$, etc.</summary>
</details>

Before moving on, we note the following property of $\Ab$-categories: If
$A$ is an object s.t. $\id_{A} = 0$, then $A$ is a zero object.
$A$ is an object s.t. $\id{A} = 0$, then $A$ is a zero object.

```agda
module _ {o ℓ} {C : Precategory o ℓ} (A : Ab-category C) where
Expand Down
2 changes: 1 addition & 1 deletion src/Cat/Abelian/Functor.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ subtraction.
```

Since the zero object $\emptyset$ in an $\Ab$-category is characterised
as the unique object having $\id_\emptyset = 0$, and $\Ab$-functors
as the unique object having $\id{\emptyset} = 0$, and $\Ab$-functors
preserve both $\id$ and $0$, every $\Ab$-functor preserves zero
objects. We say that the zero object, considered as a colimit, is
**absolute**, i.e., preserved by every (relevant) functor.
Expand Down
2 changes: 1 addition & 1 deletion src/Cat/Bi/Base.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -390,7 +390,7 @@ However, when talking about general bicategories, we are faced with a
choice: We could generalise the functoriality axioms to natural
isomorphisms, keeping with the fact that equations are invertible, but
we could also drop this invertibility requirement, and work only with
natural _transformations_ $P(\id_A) \to \id_{PA}$. When these
natural _transformations_ $P(\id{A}) \to \id{PA}$. When these
are not invertible, the resulting structure is called a **lax functor**;
When they _are_, we talk about **pseudofunctors** instead.

Expand Down
2 changes: 1 addition & 1 deletion src/Cat/Displayed/Cartesian/Discrete.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ map $u' \to a'$.
Let $x$ be an object of $\cB$. Let us ponder the fibre $\cE^*(x)$:
we know that it is strict, since by assumption there is a _set_ of
objects over $x$. Let us show also that it is thin: imagine that we have
two parallel, vertical arrows $f, g : a \to_\id b$. These assemble
two parallel, vertical arrows $f, g : a \to_{\id} b$. These assemble
into a diagram like

~~~{.quiver}
Expand Down
2 changes: 1 addition & 1 deletion src/Cat/Displayed/Fibre.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ of categories"^[Though note that unless the displayed category is a
[Cartesian fibration], this "family" might not be functorially-indexed].
Given an object $x : \cB$ of the base category, the morphisms in the
fibre over x, or **vertical morphisms**, are those in the set
$\hom_{\id_x}(x, y)$ of morphisms over the identity map (on $x$).
$\hom_{\id{x}}(x, y)$ of morphisms over the identity map (on $x$).

[Cartesian fibration]: Cat.Displayed.Cartesian.html

Expand Down
6 changes: 3 additions & 3 deletions src/Cat/Functor/Equivalence/Path.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -92,9 +92,9 @@ $f$ along $g$ to get an element of $\rm{hom}_i(x, y)$.

To obtain these definitional extensions of a morphism in C, we use
homogeneous composition, together with the functor laws. For example,
below, we obtain a line which definitionally extends $\id_\cC$ on
the left and $\id_\cD$ by gluin\idid}_\cC$ _against the
proof that $F$ preserves identity_.
below, we obtain a line which definitionally extends $\id{\cC}$ on the
left and $\id{\cD}$ by gluing $\id{\cC}$ _against the proof that $F$
preserves identity_.

```agda
idh : i x hom i x x
Expand Down
8 changes: 4 additions & 4 deletions support/shake/app/Macros.hs
Original file line number Diff line number Diff line change
Expand Up @@ -104,8 +104,8 @@ applyMacros ms s =
------------------------------------------------------------------------------

pSkipSpaceComments :: (Monad m, Stream s m Char)
=> ParsecT s st m ()
pSkipSpaceComments = spaces >> skipMany (comment >> spaces)
=> ParsecT s st m String
pSkipSpaceComments = many space <* skipMany (comment >> spaces)

pMacroDefinitions :: (Monad m, Stream s m Char)
=> ParsecT s st m ([Macro], s)
Expand Down Expand Up @@ -241,7 +241,7 @@ newcommand = try $ do
string name'
when (all isLetter name') $
notFollowedBy letter
pSkipSpaceComments
spc <- pSkipSpaceComments
opt <- case optarg of
Nothing -> return Nothing
Just _ -> liftM (`mplus` optarg) optArg
Expand All @@ -250,7 +250,7 @@ newcommand = try $ do
let args' = case opt of
Just x -> x : args
Nothing -> args
return $ apply args' $ "{" ++ body ++ "}"
return $ apply args' $ body ++ spc

return $ Macro (T.pack defn) (T.pack name) numargs kao parsec

Expand Down

0 comments on commit 26bdece

Please sign in to comment.