diff --git a/src/Cat/Bi/Instances/Relations.lagda.md b/src/Cat/Bi/Instances/Relations.lagda.md
index 28cc82560..f2bfe0bb9 100644
--- a/src/Cat/Bi/Instances/Relations.lagda.md
+++ b/src/Cat/Bi/Instances/Relations.lagda.md
@@ -48,6 +48,7 @@ monic.], but in finite-products categories, the definition takes an
 especially pleasant form: A relation $\phi : a \rel b$ is a [subobject]
 of the [Cartesian product] $a \times b$.
 
+[bicategory]: Cat.Bi.Base.html
 [regular categories]: Cat.Regular.html
 [pullback-stable]: Cat.Diagram.Pullback.html#stability
 [image factorisations]: Cat.Diagram.Image.html
diff --git a/src/Cat/Diagram/Colimit/Base.lagda.md b/src/Cat/Diagram/Colimit/Base.lagda.md
index 641f1dc1c..25cf69aca 100644
--- a/src/Cat/Diagram/Colimit/Base.lagda.md
+++ b/src/Cat/Diagram/Colimit/Base.lagda.md
@@ -663,6 +663,8 @@ coproducts indexed by its class of morphisms, then it is automatically
 [thin]. Since excluded middle is independent of type theory, we can not
 prove that any non-thin categories have arbitrary colimits.
 
+[thin]: Order.Base.html
+
 Instead, categories are cocomplete _with respect to_ a pair of
 universes: A category is **$(o, \ell)$-cocomplete** if it has colimits
 for any diagram indexed by a precategory with objects in $\ty\ o$ and
diff --git a/src/Cat/Diagram/Colimit/Cocone.lagda.md b/src/Cat/Diagram/Colimit/Cocone.lagda.md
index fb539f42e..0bbbef47d 100644
--- a/src/Cat/Diagram/Colimit/Cocone.lagda.md
+++ b/src/Cat/Diagram/Colimit/Cocone.lagda.md
@@ -150,7 +150,7 @@ We can then rephrase the universality from the definition of left Kan
 extension by asking that a particular cocone be [initial] in the
 category we have just constructed.
 
-[initial object]: Cat.Diagram.Initial.html
+[initial]: Cat.Diagram.Initial.html
 
 ```agda
   is-initial-cocone→is-colimit
diff --git a/src/Cat/Displayed/Cartesian.lagda.md b/src/Cat/Displayed/Cartesian.lagda.md
index eeb409f75..870ea8050 100644
--- a/src/Cat/Displayed/Cartesian.lagda.md
+++ b/src/Cat/Displayed/Cartesian.lagda.md
@@ -340,6 +340,7 @@ invertible→cartesian
 ```
 
 If $f$ is cartesian, it's also a [weak monomorphism].
+
 [weak monomorphism]: Cat.Displayed.Morphism.html#weak-monos
 
 ```agda
diff --git a/src/Cat/Displayed/Cartesian/Right.lagda.md b/src/Cat/Displayed/Cartesian/Right.lagda.md
index 12213e326..2a7fee03f 100644
--- a/src/Cat/Displayed/Cartesian/Right.lagda.md
+++ b/src/Cat/Displayed/Cartesian/Right.lagda.md
@@ -35,6 +35,8 @@ open Cat.Displayed.Reasoning ℰ
 A [cartesian fibration] $\cE$ is said to be a **right fibration** if every
 morphism in $\cE$ is cartesian.
 
+[cartesian fibration]: Cat.Displayed.Cartesian.html
+
 ```agda
 record Right-fibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where
   no-eta-equality
diff --git a/src/Cat/Displayed/Cocartesian/Indexing.lagda.md b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md
index 687d114e4..503da4571 100644
--- a/src/Cat/Displayed/Cocartesian/Indexing.lagda.md
+++ b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md
@@ -38,7 +38,7 @@ fibrations.
 
 [Opfibrations]: Cat.Displayed.Cocartesian.html
 [fibrations]: Cat.Displayed.Cartesian.html
-[reindex along morphisms in the base] Cat.Displayed.Cartesian.Indexing.html
+[reindex along morphisms in the base]: Cat.Displayed.Cartesian.Indexing.html
 
 This difference in variance gives opfibrations a distinct character.
 Reindexing in fibrations can be thought of a sort of restriction map.
diff --git a/src/Cat/Displayed/Cocartesian/Weak.lagda.md b/src/Cat/Displayed/Cocartesian/Weak.lagda.md
index 77fbfc9e7..d749ab0bb 100644
--- a/src/Cat/Displayed/Cocartesian/Weak.lagda.md
+++ b/src/Cat/Displayed/Cocartesian/Weak.lagda.md
@@ -473,6 +473,9 @@ record is-weak-cocartesian-fibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) wher
 -->
 
 Weak opfibrations are dual to [weak fibrations].
+
+[weak fibrations]: Cat.Displayed.Cartesian.Weak.html#is-weak-cartesian-fibration
+
 ```agda
 weak-op-fibration→weak-opfibration
   : is-weak-cartesian-fibration (ℰ ^total-op)
diff --git a/src/Cat/Displayed/Composition.lagda.md b/src/Cat/Displayed/Composition.lagda.md
index 775b32844..c269f0dee 100644
--- a/src/Cat/Displayed/Composition.lagda.md
+++ b/src/Cat/Displayed/Composition.lagda.md
@@ -26,7 +26,7 @@ $\int \cE$, then we can construct a new category $\cE \cdot \cF$
 displayed over $\cB$ that contains the data of both $\cE$ and
 $\cF$.
 
-[total category] Cat.Displayed.Total.html
+[total category]: Cat.Displayed.Total.html
 
 To actually construct the composite, we bundle up the data of
 $\cE$ and $\cF$ into pairs, so an object in $\cE \cdot \cF$
diff --git a/src/Cat/Displayed/GenericObject.lagda.md b/src/Cat/Displayed/GenericObject.lagda.md
index 99556f01c..aabf52e5b 100644
--- a/src/Cat/Displayed/GenericObject.lagda.md
+++ b/src/Cat/Displayed/GenericObject.lagda.md
@@ -158,10 +158,10 @@ structure of $t'$.
 
 This condition is quite strong: for instance, the family fibration of a
 strict category $\cC$ has a skeletal generic object if and only if $\cC$
-is [skeletal] (See [here] for a proof).
+is [skeletal] (See [here](Cat.Displayed.Instances.Family.html#skeletal-generic-objects)
+for a proof).
 
 [skeletal]: Cat.Skeletal.html
-[here]: Cat.Displayed.Instances.Family.html#skeletal-generic-objects
 
 ```agda
 is-skeletal-generic-object : ∀ {t} {t′ : Ob[ t ]} → Generic-object t′ → Type _
@@ -194,10 +194,10 @@ must, as well.
 
 We can also expand on what this means for the family fibration:
 $\rm{Fam}({\cC})$ has a gaunt generic object if and only if $\cC$ is itself
-[gaunt] (See [here] for the proof).
+[gaunt] (See [here](Cat.Displayed.Instances.Family.html#gaunt-generic-objects)
+for the proof).
 
 [gaunt]: Cat.Gaunt.html
-[here]: Cat.Displayed.Instances.Family.html#gaunt-generic-objects
 
 <!--
 ```agda
diff --git a/src/Cat/Displayed/Univalence/Thin.lagda.md b/src/Cat/Displayed/Univalence/Thin.lagda.md
index 3c2db87d4..cbc770a06 100644
--- a/src/Cat/Displayed/Univalence/Thin.lagda.md
+++ b/src/Cat/Displayed/Univalence/Thin.lagda.md
@@ -37,7 +37,7 @@ open _≅[_]_
 # Thinly displayed structures
 
 The HoTT Book's version of the structure identity principle can be seen
-as a very early example of displayed category theory. Their notion of
+as a very early example of displayed category theory. Their
 _standard notion of structure_ corresponds exactly to a displayed
 category, all of whose fibres are posets. Note that this is not a
 category _fibred in_ posets, since the displayed category will not
@@ -51,6 +51,8 @@ of note not only because they intersect the categorical SIP defined
 above with the [typal SIP] established in the prelude modules, but also
 because we can work with them very directly.
 
+[typal SIP]: 1Lab.Univalence.SIP.html
+
 ```agda
 record
   Thin-structure {ℓ o′} ℓ′ (S : Type ℓ → Type o′)
diff --git a/src/Cat/Instances/InternalFunctor/Compose.lagda.md b/src/Cat/Instances/InternalFunctor/Compose.lagda.md
index 4396aa351..a90b72f15 100644
--- a/src/Cat/Instances/InternalFunctor/Compose.lagda.md
+++ b/src/Cat/Instances/InternalFunctor/Compose.lagda.md
@@ -20,6 +20,7 @@ Internal functor composition is functorial, when viewed as an operation
 on [internal functor categories]. This mirrors [the similar results] for
 composition of ordinary functors.
 
+[internal functor categories]: Cat.Instances.InternalFunctor.html
 [the similar results]: Cat.Instances.Functor.Compose.html
 
 To show this, we will need to define whiskering and horizontal
diff --git a/src/Cat/Internal/Base.lagda.md b/src/Cat/Internal/Base.lagda.md
index cf58a16fb..902a158f5 100644
--- a/src/Cat/Internal/Base.lagda.md
+++ b/src/Cat/Internal/Base.lagda.md
@@ -32,6 +32,8 @@ is a category with [pullbacks], fix a pair of objects $\bC_0, \bC_1$ be
 a pair of objects, and parallel maps $\$1, \$1 : \bC_1 \to
 \bC_0$.
 
+[pullbacks]: Cat.Diagram.Pullback.html
+
 The idea is that $\bC_0$ and $\bC_1$ are meant to be the "object of
 objects" and "object of morphisms", respectively, while the maps
 $\$1$ and $\$1$ maps assign each morphism to its domain and
diff --git a/src/Cat/Internal/Sets.lagda.md b/src/Cat/Internal/Sets.lagda.md
index dca8f80c1..35bf808c0 100644
--- a/src/Cat/Internal/Sets.lagda.md
+++ b/src/Cat/Internal/Sets.lagda.md
@@ -21,7 +21,7 @@ precategories with a `Set`{.Agda ident=is-set} of objects. Starting from
 a category $\bC$ internal to $\Sets$ and ending up with a strict
 category is quite unremarkable:
 
-[strict]: Cat.Strict.html
+[strict categories]: Cat.Strict.html
 
 ```agda
 Internal-cat→Precategory : ∀ {κ} → Internal-cat (Sets κ) → Precategory κ κ
diff --git a/src/Cat/Morphism/StrongEpi.lagda.md b/src/Cat/Morphism/StrongEpi.lagda.md
index 2cc3461ca..b541a6eb5 100644
--- a/src/Cat/Morphism/StrongEpi.lagda.md
+++ b/src/Cat/Morphism/StrongEpi.lagda.md
@@ -188,7 +188,7 @@ epimorphism", we'd certainly like regular epis to be strong epis!
 
 This is fortunately the case. Suppose that $f : a \to b$ is the
 coequaliser of some maps $s, t : r \to a$^[If you care, $r$ is for
-"relation" --- the intution is that $r$ specifies the _relations_
+"relation" --- the intuition is that $r$ specifies the _relations_
 imposed on $a$ to get $b$], and that $z : c \mono b$ is a monomorphism
 we want to lift against.
 
@@ -437,6 +437,7 @@ along $m$ to obtain the square
   \arrow["e", curve={height=-12pt}, from=1-1, to=3-5]
   \arrow["u", curve={height=12pt}, from=1-1, to=5-3]
 \end{tikzcd}\]
+~~~
 
 and obtain the unique factorisation $A \to A \times_D B$. Note that the
 map $u : A \times_D B \mono B$ is a monomorphism since it results from
diff --git a/src/Cat/Regular/Slice.lagda.md b/src/Cat/Regular/Slice.lagda.md
index 632b9967e..190f518b8 100644
--- a/src/Cat/Regular/Slice.lagda.md
+++ b/src/Cat/Regular/Slice.lagda.md
@@ -37,6 +37,7 @@ passing to arbitrary contexts.
 [pullback-stable]: Cat.Diagram.Pullback.html#stability
 [strong epi]: Cat.Morphism.StrongEpi.html
 [mono]: Cat.Morphism.html#monos
+[slice]: Cat.Instances.Slice.html
 [finitely complete]: Cat.Diagram.Limit.Finite.html
 
 <!--
diff --git a/src/Data/Image.lagda.md b/src/Data/Image.lagda.md
index 504f347fb..d793223c8 100644
--- a/src/Data/Image.lagda.md
+++ b/src/Data/Image.lagda.md
@@ -165,6 +165,8 @@ should be
 3. With a constructor coherently mapping proofs of $f'(x) \sim f'(y)$ to
 $x \equiv y$.
 
+[identity system]: 1Lab.Path.IdentitySystem.html
+
 But, identity system or not, this is hopeless, right? We don't know how
 to specify $\im f$ without first defining $f'$; and it makes no sense to
 define $f'$ before its domain type. The only way forward would be to
diff --git a/src/Prim/Interval.lagda.md b/src/Prim/Interval.lagda.md
index ee46cbbdf..51474b697 100644
--- a/src/Prim/Interval.lagda.md
+++ b/src/Prim/Interval.lagda.md
@@ -79,10 +79,10 @@ postulate
 
 The `IsOne`{.Agda} proposition is used as the domain of the type
 `Partial`{.Agda}, where `Partial φ A` is a refinement of the type
-`.(IsOne φ) → A`^[domfinite], where inhabitants `p, q : Partial φ A` are
+`.(IsOne φ) → A`[^domfinite], where inhabitants `p, q : Partial φ A` are
 equal iff they agree on a decomposition of `φ` into DNF.
 
-[domfinite]: They're actually equal, but this is [a
+[^domfinite]: They're actually equal, but this is [a
 bug](https://github.com/agda/agda/issues/6015).
 
 ```agda
diff --git a/support/shake/app/Shake/LinkReferences.hs b/support/shake/app/Shake/LinkReferences.hs
index a0c7f5a81..a676e1029 100644
--- a/support/shake/app/Shake/LinkReferences.hs
+++ b/support/shake/app/Shake/LinkReferences.hs
@@ -43,7 +43,7 @@ linkReferences modname (Pandoc meta blocks) = Pandoc meta (walk link blocks)
 
 renderReference :: Reference -> Text -> Inline
 renderReference (Reference href cls) t =
-  Span ("", ["Agda"], []) [Link ("", [cls], []) [Str t] (href, "")]
+  Span ("", ["Agda"], []) [Link ("", [cls], []) [Code nullAttr t] (href, "")]
 
 data Reference =
   Reference { refHref  :: Text
diff --git a/support/shake/app/Shake/Markdown.hs b/support/shake/app/Shake/Markdown.hs
index 145b4e75d..aad1a1d18 100644
--- a/support/shake/app/Shake/Markdown.hs
+++ b/support/shake/app/Shake/Markdown.hs
@@ -185,6 +185,10 @@ patchInline _ autolinks (RawInline "tex" txt)
   , let key = Text.take (Text.length txt' - 1) txt'
   , Just target <- Map.lookup (Text.toLower key) autolinks
   = pure $ Link ("", [], []) (intersperse Space $ map Str (Text.words key)) (target, key)
+patchInline _ _ (Str s)
+  | "[" `Text.isPrefixOf` s
+  , s /= "[", s /= "[…]" -- "[" appears on its own before citations
+  = error ("possible broken link: " <> Text.unpack s)
 patchInline _ _ h = pure h