diff --git a/src/plfa/Bisimulation.lagda.md b/src/plfa/Bisimulation.lagda.md
index b1cbb273..11ab3ba4 100644
--- a/src/plfa/Bisimulation.lagda.md
+++ b/src/plfa/Bisimulation.lagda.md
@@ -119,14 +119,14 @@ above is a simulation from source to target.  We leave
 establishing it in the reverse direction as an exercise.
 Another exercise is to show the alternative formulations
 of products in
-Chapter [More][plfa.More]
+Chapter [More]({{ site.baseurl }}/More/)
 are in bisimulation.
 
 
 ## Imports
 
 We import our source language from
-Chapter [More][plfa.More]:
+Chapter [More]({{ site.baseurl }}/More/):
 ```
 open import plfa.More
 ```
@@ -164,7 +164,7 @@ data _~_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
       ----------------------
     → `let M N ~ (ƛ N†) · M†
 ```
-The language in Chapter [More][plfa.More] has more constructs, which we could easily add.
+The language in Chapter [More]({{ site.baseurl }}/More/) has more constructs, which we could easily add.
 However, leaving the simulation small let's us focus on the essence.
 It's a handy technical trick that we can have a large source language,
 but only bother to include in the simulation the terms of interest.
@@ -468,7 +468,7 @@ a bisimulation.
 #### Exercise `products`
 
 Show that the two formulations of products in
-Chapter [More][plfa.More]
+Chapter [More]({{ site.baseurl }}/More/)
 are in bisimulation.  The only constructs you need to include are
 variables, and those connected to functions and products.
 In this case, the simulation is _not_ lock-step.
diff --git a/src/plfa/Connectives.lagda.md b/src/plfa/Connectives.lagda.md
index 7331baec..64010ff7 100644
--- a/src/plfa/Connectives.lagda.md
+++ b/src/plfa/Connectives.lagda.md
@@ -234,7 +234,7 @@ corresponds to `⟨ 1 , ⟨ true , aa ⟩ ⟩`, which is a member of the latter.
 
 #### Exercise `⇔≃×` (recommended)
 
-Show that `A ⇔ B` as defined [earlier][plfa.Isomorphism#iff]
+Show that `A ⇔ B` as defined [earlier]({{ site.baseurl }}/Isomorphism/#iff)
 is isomorphic to `(A → B) × (B → A)`.
 
 ```
@@ -770,9 +770,9 @@ The standard library constructs pairs with `_,_` whereas we use `⟨_,_⟩`.
 The former makes it convenient to build triples or larger tuples from pairs,
 permitting `a , b , c` to stand for `(a , (b , c))`.  But it conflicts with
 other useful notations, such as `[_,_]` to construct a list of two elements in
-Chapter [Lists][plfa.Lists]
+Chapter [Lists]({{ site.baseurl }}/Lists/)
 and `Γ , A` to extend environments in
-Chapter [DeBruijn][plfa.DeBruijn].
+Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/).
 The standard library `_⇔_` is similar to ours, but the one in the
 standard library is less convenient, since it is parameterised with
 respect to an arbitrary notion of equivalence.
diff --git a/src/plfa/DeBruijn.lagda.md b/src/plfa/DeBruijn.lagda.md
index ae237ed2..3e947abe 100644
--- a/src/plfa/DeBruijn.lagda.md
+++ b/src/plfa/DeBruijn.lagda.md
@@ -56,10 +56,10 @@ And here is its corresponding type derivation:
       ∋z = Z
 
 (These are both taken from Chapter
-[Lambda][plfa.Lambda]
+[Lambda]({{ site.baseurl }}/Lambda/)
 and you can see the corresponding derivation tree written out
 in full
-[here][plfa.Lambda#derivation].)
+[here]({{ site.baseurl }}/Lambda/#derivation).)
 The two definitions are in close correspondence, where:
 
   * `` `_ `` corresponds to `` ⊢` ``
@@ -112,7 +112,7 @@ typed terms, which in context `Γ` have type `A`.
 While these two choices fit well, they are independent.  One
 can use de Bruijn indices in raw terms, or (with more
 difficulty) have inherently typed terms with names.  In
-Chapter [Untyped][plfa.Untyped],
+Chapter [Untyped]({{ site.baseurl }}/Untyped/),
 we will introduce terms with de Bruijn indices that
 are inherently scoped but not typed.
 
@@ -408,7 +408,7 @@ lookup ∅       _        =  ⊥-elim impossible
 We intend to apply the function only when the natural is
 shorter than the length of the context, which we indicate by
 postulating an `impossible` term, just as we did
-[here][plfa.Lambda#impossible].
+[here]({{ site.baseurl }}/Lambda/#impossible).
 
 Given the above, we can convert a natural to a corresponding
 de Bruijn index, looking up its type in the context:
@@ -437,9 +437,9 @@ _ = ƛ ƛ (# 1 · (# 1 · # 0))
 ### Test examples
 
 We repeat the test examples from
-Chapter [Lambda][plfa.Lambda].
+Chapter [Lambda]({{ site.baseurl }}/Lambda/).
 You can find them
-[here][plfa.Lambda#derivation]
+[here]({{ site.baseurl }}/Lambda/#derivation)
 for comparison.
 
 First, computing two plus two on naturals:
@@ -772,7 +772,7 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where
 
 Here `zero` requires an implicit parameter to aid inference,
 much in the same way that `[]` did in
-[Lists][plfa.Lists].
+[Lists]({{ site.baseurl }}/Lists/).
 
 
 ## Reduction
diff --git a/src/plfa/Decidable.lagda.md b/src/plfa/Decidable.lagda.md
index c8849be9..185c9a6b 100644
--- a/src/plfa/Decidable.lagda.md
+++ b/src/plfa/Decidable.lagda.md
@@ -39,7 +39,7 @@ open import plfa.Isomorphism using (_⇔_)
 
 ## Evidence vs Computation
 
-Recall that Chapter [Relations][plfa.Relations]
+Recall that Chapter [Relations]({{ site.baseurl }}/Relations/)
 defined comparison as an inductive datatype,
 which provides _evidence_ that one number
 is less than or equal to another:
@@ -548,7 +548,7 @@ postulate
 #### Exercise `iff-erasure` (recommended)
 
 Give analogues of the `_⇔_` operation from
-Chapter [Isomorphism][plfa.Isomorphism#iff],
+Chapter [Isomorphism]({{ site.baseurl }}/Isomorphism/#iff),
 operation on booleans and decidables, and also show the corresponding erasure:
 ```
 postulate
diff --git a/src/plfa/Equality.lagda.md b/src/plfa/Equality.lagda.md
index 5a372529..4d6db1dc 100644
--- a/src/plfa/Equality.lagda.md
+++ b/src/plfa/Equality.lagda.md
@@ -347,7 +347,7 @@ an order that will make sense to the reader.
 #### Exercise `≤-Reasoning` (stretch)
 
 The proof of monotonicity from
-Chapter [Relations][plfa.Relations]
+Chapter [Relations]({{ site.baseurl }}/Relations/)
 can be written in a more readable form by using an analogue of our
 notation for `≡-Reasoning`.  Define `≤-Reasoning` analogously, and use
 it to write out an alternative proof that addition is monotonic with
diff --git a/src/plfa/Induction.lagda.md b/src/plfa/Induction.lagda.md
index 6815f776..07f11f3d 100644
--- a/src/plfa/Induction.lagda.md
+++ b/src/plfa/Induction.lagda.md
@@ -366,7 +366,7 @@ proof of associativity.
 
 The symbol `∀` appears in the statement of associativity to indicate that
 it holds for all numbers `m`, `n`, and `p`.  We refer to `∀` as the _universal
-quantifier_, and it is discussed further in Chapter [Quantifiers][plfa.Quantifiers].
+quantifier_, and it is discussed further in Chapter [Quantifiers]({{ site.baseurl }}/Quantifiers/).
 
 Evidence for a universal quantifier is a function.  The notations
 
@@ -697,11 +697,11 @@ judgments where the first number is less than _m_.
 There is also a completely finite approach to generating the same equations,
 which is left as an exercise for the reader.
 
-#### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc}
+#### Exercise `finite-|-assoc` (stretch) {#finite-plus-assoc}
 
 Write out what is known about associativity of addition on each of the
 first four days using a finite story of creation, as
-[earlier][plfa.Naturals#finite-creation].
+[earlier]({{ site.baseurl }}/Naturals/#finite-creation).
 
 ```
 -- Your code goes here
@@ -927,7 +927,7 @@ for all naturals `n`. Did your proof require induction?
 ```
 
 
-#### Exercise `∸-+-assoc` {#monus-plus-assoc}
+#### Exercise `∸-|-assoc` {#monus-plus-assoc}
 
 Show that monus associates with addition, that is,
 
@@ -954,7 +954,7 @@ for all `m`, `n`, and `p`.
 #### Exercise `Bin-laws` (stretch) {#Bin-laws}
 
 Recall that
-Exercise [Bin][plfa.Naturals#Bin]
+Exercise [Bin]({{ site.baseurl }}/Naturals/#Bin)
 defines a datatype of bitstrings representing natural numbers
 ```
 data Bin : Set where
diff --git a/src/plfa/Inference.lagda.md b/src/plfa/Inference.lagda.md
index a9036d90..7e65eb04 100644
--- a/src/plfa/Inference.lagda.md
+++ b/src/plfa/Inference.lagda.md
@@ -12,9 +12,9 @@ module plfa.Inference where
 
 So far in our development, type derivations for the corresponding
 term have been provided by fiat.
-In Chapter [Lambda][plfa.Lambda]
+In Chapter [Lambda]({{ site.baseurl }}/Lambda/)
 type derivations were given separately from the term, while
-in Chapter [DeBruijn][plfa.DeBruijn]
+in Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/)
 the type derivation was inherently part of the term.
 
 In practice, one often writes down a term with a few decorations and
@@ -27,9 +27,9 @@ inference, which will be presented in this chapter.
 
 This chapter ties our previous developments together. We begin with
 a term with some type annotations, quite close to the raw terms of
-Chapter [Lambda][plfa.Lambda],
+Chapter [Lambda]({{ site.baseurl }}/Lambda/),
 and from it we compute a term with inherent types, in the style of
-Chapter [DeBruijn][plfa.DeBruijn].
+Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/).
 
 ## Introduction: Inference rules as algorithms {#algorithms}
 
@@ -382,7 +382,7 @@ required for `sucᶜ`, which inherits its type as an argument of `plusᶜ`.
 ## Bidirectional type checking
 
 The typing rules for variables are as in
-[Lambda][plfa.Lambda]:
+[Lambda]({{ site.baseurl }}/Lambda/):
 ```
 data _∋_⦂_ : Context → Id → Type → Set where
 
@@ -456,25 +456,25 @@ data _⊢_↓_ where
     → Γ ⊢ (M ↑) ↓ B
 ```
 We follow the same convention as
-Chapter [Lambda][plfa.Lambda],
+Chapter [Lambda]({{ site.baseurl }}/Lambda/),
 prefacing the constructor with `⊢` to derive the name of the
 corresponding type rule.
 
 The rules are similar to those in
-Chapter [Lambda][plfa.Lambda],
+Chapter [Lambda]({{ site.baseurl }}/Lambda/),
 modified to support synthesised and inherited types.
 The two new rules are those for `⊢↑` and `⊢↓`.
 The former both passes the type decoration as the inherited type and returns
 it as the synthesised type.  The latter takes the synthesised type and the
 inherited type and confirms they are identical --- it should remind you of
 the equality test in the application rule in the first
-[section][plfa.Inference#algorithms].
+[section]({{ site.baseurl }}/Inference/#algorithms).
 
 
 #### Exercise `bidirectional-mul` (recommended) {#bidirectional-mul}
 
 Rewrite your definition of multiplication from
-Chapter [Lambda][plfa.Lambda], decorated to support inference.
+Chapter [Lambda]({{ site.baseurl }}/Lambda/), decorated to support inference.
 
 ```
 -- Your code goes here
@@ -484,7 +484,7 @@ Chapter [Lambda][plfa.Lambda], decorated to support inference.
 #### Exercise `bidirectional-products` (recommended) {#bidirectional-products}
 
 Extend the bidirectional type rules to include products from
-Chapter [More][plfa.More].
+Chapter [More]({{ site.baseurl }}/More/).
 
 ```
 -- Your code goes here
@@ -494,7 +494,7 @@ Chapter [More][plfa.More].
 #### Exercise `bidirectional-rest` (stretch)
 
 Extend the bidirectional type rules to include the rest of the constructs from
-Chapter [More][plfa.More].
+Chapter [More]({{ site.baseurl }}/More/).
 
 ```
 -- Your code goes here
@@ -1004,7 +1004,7 @@ _ = refl
 From the evidence that a decorated term has the correct type it is
 easy to extract the corresponding inherently typed term.  We use the
 name `DB` to refer to the code in
-Chapter [DeBruijn][plfa.DeBruijn].
+Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/).
 It is easy to define an _erasure_ function that takes evidence of a
 type judgment into the corresponding inherently typed term.
 
@@ -1067,17 +1067,17 @@ _ = refl
 ```
 Thus, we have confirmed that bidirectional type inference
 converts decorated versions of the lambda terms from
-Chapter [Lambda][plfa.Lambda]
+Chapter [Lambda]({{ site.baseurl }}/Lambda/)
 to the inherently typed terms of
-Chapter [DeBruijn][plfa.DeBruijn].
+Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/).
 
 
 #### Exercise `inference-multiplication` (recommended)
 
 Apply inference to your decorated definition of multiplication from
-exercise [`bidirectional-mul`][plfa.Inference#bidirectional-mul], and show that
+exercise [`bidirectional-mul`]({{ site.baseurl }}/Inference/#bidirectional-mul), and show that
 erasure of the inferred typing yields your definition of
-multiplication from Chapter [DeBruijn][plfa.DeBruijn].
+multiplication from Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/).
 
 ```
 -- Your code goes here
@@ -1086,7 +1086,7 @@ multiplication from Chapter [DeBruijn][plfa.DeBruijn].
 #### Exercise `inference-products` (recommended)
 
 Using your rules from exercise
-[`bidirectional-products`][plfa.Inference#bidirectional-products], extend
+[`bidirectional-products`]({{ site.baseurl }}/Inference/#bidirectional-products), extend
 bidirectional inference to include products.
 
 ```
@@ -1096,7 +1096,7 @@ bidirectional inference to include products.
 #### Exercise `inference-rest` (stretch)
 
 Extend the bidirectional type rules to include the rest of the constructs from
-Chapter [More][plfa.More].
+Chapter [More]({{ site.baseurl }}/More/).
 
 ```
 -- Your code goes here
diff --git a/src/plfa/Isomorphism.lagda.md b/src/plfa/Isomorphism.lagda.md
index 3c45b53a..dd22ef9c 100644
--- a/src/plfa/Isomorphism.lagda.md
+++ b/src/plfa/Isomorphism.lagda.md
@@ -89,7 +89,7 @@ Extensionality asserts that the only way to distinguish functions is
 by applying them; if two functions applied to the same argument always
 yield the same result, then they are the same function.  It is the
 converse of `cong-app`, as introduced
-[earlier][plfa.Equality#cong].
+[earlier]({{ site.baseurl }}/Equality/#cong).
 
 Agda does not presume extensionality, but we can postulate that it holds:
 ```
@@ -104,7 +104,7 @@ known to be consistent with the theory that underlies Agda.
 
 As an example, consider that we need results from two libraries,
 one where addition is defined, as in
-Chapter [Naturals][plfa.Naturals],
+Chapter [Naturals]({{ site.baseurl }}/Naturals/),
 and one where it is defined the other way around.
 ```
 _+′_ : ℕ → ℕ → ℕ
@@ -456,8 +456,8 @@ Show that equivalence is reflexive, symmetric, and transitive.
 #### Exercise `Bin-embedding` (stretch) {#Bin-embedding}
 
 Recall that Exercises
-[Bin][plfa.Naturals#Bin] and
-[Bin-laws][plfa.Induction#Bin-laws]
+[Bin]({{ site.baseurl }}/Naturals/#Bin) and
+[Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws)
 define a datatype of bitstrings representing natural numbers:
 ```
 data Bin : Set where
diff --git a/src/plfa/Lambda.lagda.md b/src/plfa/Lambda.lagda.md
index 4433216f..76ca8ff6 100644
--- a/src/plfa/Lambda.lagda.md
+++ b/src/plfa/Lambda.lagda.md
@@ -25,7 +25,7 @@ recursive function definitions.
 
 This chapter formalises the simply-typed lambda calculus, giving its
 syntax, small-step semantics, and typing rules.  The next chapter
-[Properties][plfa.Properties]
+[Properties]({{ site.baseurl }}/Properties/)
 proves its main properties, including
 progress and preservation.  Following chapters will look at a number
 of variants of lambda calculus.
@@ -33,7 +33,7 @@ of variants of lambda calculus.
 Be aware that the approach we take here is _not_ our recommended
 approach to formalisation.  Using de Bruijn indices and
 inherently-typed terms, as we will do in
-Chapter [DeBruijn][plfa.DeBruijn],
+Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/),
 leads to a more compact formulation.  Nonetheless, we begin with named
 variables, partly because such terms are easier to read and partly
 because the development is more traditional.
@@ -138,7 +138,7 @@ plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
 ```
 The recursive definition of addition is similar to our original
 definition of `_+_` for naturals, as given in
-Chapter [Naturals][plfa.Naturals#plus].
+Chapter [Naturals]({{ site.baseurl }}/Naturals/#plus).
 Here variable "m" is bound twice, once in a lambda abstraction and once in
 the successor branch of the case; the first use of "m" refers to
 the former and the second to the latter.  Any use of "m" in the successor branch
@@ -373,7 +373,7 @@ to treat variables as values, and to treat
 `ƛ x ⇒ N` as a value only if `N` is a value.
 Indeed, this is how Agda normalises terms.
 We consider this approach in
-Chapter [Untyped][plfa.Untyped].
+Chapter [Untyped]({{ site.baseurl }}/Untyped/).
 
 
 ## Substitution
@@ -678,7 +678,7 @@ the reflexive and transitive closure `—↠` of the step relation `—→`.
 We define reflexive and transitive closure as a sequence of zero or
 more steps of the underlying relation, along lines similar to that for
 reasoning about chains of equalities in
-Chapter [Equality][plfa.Equality]:
+Chapter [Equality]({{ site.baseurl }}/Equality/):
 ```
 infix  2 _—↠_
 infix  1 begin_
@@ -1310,7 +1310,7 @@ We can fill in `Z` by hand. If we type C-c C-space, Agda will confirm we are don
 
 The entire process can be automated using Agsy, invoked with C-c C-a.
 
-Chapter [Inference][plfa.Inference]
+Chapter [Inference]({{ site.baseurl }}/Inference/)
 will show how to use Agda to compute type derivations directly.
 
 
diff --git a/src/plfa/Lists.lagda.md b/src/plfa/Lists.lagda.md
index f45c3186..77c763a5 100644
--- a/src/plfa/Lists.lagda.md
+++ b/src/plfa/Lists.lagda.md
@@ -178,7 +178,7 @@ and follows by straightforward computation combined with the
 inductive hypothesis.  As usual, the inductive hypothesis is indicated by a recursive
 invocation of the proof, in this case `++-assoc xs ys zs`.
 
-Recall that Agda supports [sections][plfa.Induction#sections].
+Recall that Agda supports [sections]({{ site.baseurl }}/Induction/#sections).
 Applying `cong (x ∷_)` promotes the inductive hypothesis:
 
     (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
@@ -932,7 +932,7 @@ Show that the equivalence `All-++-⇔` can be extended to an isomorphism.
 #### Exercise `¬Any≃All¬` (stretch)
 
 First generalise composition to arbitrary levels, using
-[universe polymorphism][plfa.Equality#unipoly]:
+[universe polymorphism]({{ site.baseurl }}/Equality/#unipoly):
 ```
 _∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
   → (B → C) → (A → B) → A → C
diff --git a/src/plfa/More.lagda.md b/src/plfa/More.lagda.md
index 1877337c..b0254a9b 100644
--- a/src/plfa/More.lagda.md
+++ b/src/plfa/More.lagda.md
@@ -31,10 +31,10 @@ informal. We show how to formalise the first four constructs and leave
 the rest as an exercise for the reader.
 
 Our informal descriptions will be in the style of
-Chapter [Lambda][plfa.Lambda],
+Chapter [Lambda]({{ site.baseurl }}/Lambda/),
 using named variables and a separate type relation,
 while our formalisation will be in the style of
-Chapter [DeBruijn][plfa.DeBruijn],
+Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/),
 using de Bruijn indices and inherently typed terms.
 
 By now, explaining with symbols should be more concise, more precise,
diff --git a/src/plfa/Naturals.lagda.md b/src/plfa/Naturals.lagda.md
index 22e23e61..9f6b64dd 100644
--- a/src/plfa/Naturals.lagda.md
+++ b/src/plfa/Naturals.lagda.md
@@ -277,7 +277,7 @@ all the names specified in the `using` clause into the current scope.
 In this case, the names added are `begin_`, `_≡⟨⟩_`, and `_∎`.  We
 will see how these are used below.  We take these as givens for now,
 but will see how they are defined in
-Chapter [Equality][plfa.Equality].
+Chapter [Equality]({{ site.baseurl }}/Equality/).
 
 Agda uses underbars to indicate where terms appear in infix or mixfix
 operators. Thus, `_≡_` and `_≡⟨⟩_` are infix (each operator is written
diff --git a/src/plfa/Negation.lagda.md b/src/plfa/Negation.lagda.md
index f2e1b63c..1d989cba 100644
--- a/src/plfa/Negation.lagda.md
+++ b/src/plfa/Negation.lagda.md
@@ -189,7 +189,7 @@ again causing the equality to hold trivially.
 #### Exercise `<-irreflexive` (recommended)
 
 Using negation, show that
-[strict inequality][plfa.Relations#strict-inequality]
+[strict inequality]({{ site.baseurl }}/Relations/#strict-inequality)
 is irreflexive, that is, `n < n` holds for no `n`.
 
 ```
@@ -200,7 +200,7 @@ is irreflexive, that is, `n < n` holds for no `n`.
 #### Exercise `trichotomy`
 
 Show that strict inequality satisfies
-[trichotomy][plfa.Relations#trichotomy],
+[trichotomy]({{ site.baseurl }}/Relations/#trichotomy),
 that is, for any naturals `m` and `n` exactly one of the following holds:
 
 * `m < n`
diff --git a/src/plfa/Quantifiers.lagda.md b/src/plfa/Quantifiers.lagda.md
index bdfcc233..78a8bd1c 100644
--- a/src/plfa/Quantifiers.lagda.md
+++ b/src/plfa/Quantifiers.lagda.md
@@ -90,7 +90,7 @@ postulate
     (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
 ```
 Compare this with the result (`→-distrib-×`) in
-Chapter [Connectives][plfa.Connectives].
+Chapter [Connectives]({{ site.baseurl }}/Connectives/).
 
 #### Exercise `⊎∀-implies-∀⊎`
 
@@ -233,7 +233,7 @@ Indeed, the converse also holds, and the two together form an isomorphism:
 ```
 The result can be viewed as a generalisation of currying.  Indeed, the code to
 establish the isomorphism is identical to what we wrote when discussing
-[implication][plfa.Connectives#implication].
+[implication]({{ site.baseurl }}/Connectives/#implication).
 
 #### Exercise `∃-distrib-⊎` (recommended)
 
@@ -263,7 +263,7 @@ Show that `∃[ x ] B x` is isomorphic to `B aa ⊎ B bb ⊎ B cc`.
 ## An existential example
 
 Recall the definitions of `even` and `odd` from
-Chapter [Relations][plfa.Relations]:
+Chapter [Relations]({{ site.baseurl }}/Relations/):
 ```
 data even : ℕ → Set
 data odd  : ℕ → Set
@@ -371,7 +371,7 @@ restated in this way.
 -- Your code goes here
 ```
 
-#### Exercise `∃-+-≤`
+#### Exercise `∃-|-≤`
 
 Show that `y ≤ z` holds if and only if there exists a `x` such that
 `x + y ≡ z`.
@@ -432,9 +432,9 @@ Does the converse hold? If so, prove; if not, explain why.
 #### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism}
 
 Recall that Exercises
-[Bin][plfa.Naturals#Bin],
-[Bin-laws][plfa.Induction#Bin-laws], and
-[Bin-predicates][plfa.Relations#Bin-predicates]
+[Bin]({{ site.baseurl }}/Naturals/#Bin),
+[Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws), and
+[Bin-predicates]({{ site.baseurl }}/Relations/#Bin-predicates)
 define a datatype of bitstrings representing natural numbers:
 ```
 data Bin : Set where
diff --git a/src/plfa/Relations.lagda.md b/src/plfa/Relations.lagda.md
index e9f98a45..ea158e1c 100644
--- a/src/plfa/Relations.lagda.md
+++ b/src/plfa/Relations.lagda.md
@@ -155,7 +155,7 @@ either `(1 ≤ 2) ≤ 3` or `1 ≤ (2 ≤ 3)`.
 Given two numbers, it is straightforward to compute whether or not the
 first is less than or equal to the second.  We don't give the code for
 doing so here, but will return to this point in
-Chapter [Decidable][plfa.Decidable].
+Chapter [Decidable]({{ site.baseurl }}/Decidable/).
 
 
 ## Inversion
@@ -377,7 +377,7 @@ evidence of `m ≤ n` and `n ≤ m` respectively.
 
 (For those familiar with logic, the above definition
 could also be written as a disjunction. Disjunctions will
-be introduced in Chapter [Connectives][plfa.Connectives].)
+be introduced in Chapter [Connectives]({{ site.baseurl }}/Connectives/).)
 
 This is our first use of a datatype with _parameters_,
 in this case `m` and `n`.  It is equivalent to the following
@@ -572,7 +572,7 @@ It is also monotonic with regards to addition and multiplication.
 Most of the above are considered in exercises below.  Irreflexivity
 requires negation, as does the fact that the three cases in
 trichotomy are mutually exclusive, so those points are deferred to
-Chapter [Negation][plfa.Negation].
+Chapter [Negation]({{ site.baseurl }}/Negation/).
 
 It is straightforward to show that `suc m ≤ n` implies `m < n`,
 and conversely.  One can then give an alternative derivation of the
@@ -599,7 +599,7 @@ Define `m > n` to be the same as `n < m`.
 You will need a suitable data declaration,
 similar to that used for totality.
 (We will show that the three cases are exclusive after we introduce
-[negation][plfa.Negation].)
+[negation]({{ site.baseurl }}/Negation/).)
 
 ```
 -- Your code goes here
@@ -742,7 +742,7 @@ Show that the sum of two odd numbers is even.
 #### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
 
 Recall that
-Exercise [Bin][plfa.Naturals#Bin]
+Exercise [Bin]({{ site.baseurl }}/Naturals/#Bin)
 defines a datatype `Bin` of bitstrings representing natural numbers.
 Representations are not unique due to leading zeros.
 Hence, eleven may be represented by both of the following:
@@ -801,7 +801,7 @@ import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
 ```
 In the standard library, `≤-total` is formalised in terms of
 disjunction (which we define in
-Chapter [Connectives][plfa.Connectives]),
+Chapter [Connectives]({{ site.baseurl }}/Connectives/)),
 and `+-monoʳ-≤`, `+-monoˡ-≤`, `+-mono-≤` are proved differently than here,
 and more arguments are implicit.
 
diff --git a/src/plfa/Untyped.lagda.md b/src/plfa/Untyped.lagda.md
index 31a85785..947f1ad9 100644
--- a/src/plfa/Untyped.lagda.md
+++ b/src/plfa/Untyped.lagda.md
@@ -62,7 +62,7 @@ open import Relation.Nullary.Product using (_×-dec_)
 ## Untyped is Uni-typed
 
 Our development will be close to that in
-Chapter [DeBruijn][plfa.DeBruijn],
+Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/),
 save that every term will have exactly the same type, written `★`
 and pronounced "any".
 This matches a slogan introduced by Dana Scott
@@ -756,7 +756,7 @@ Confirm that two times two is four.
 #### Exercise `encode-more` (stretch)
 
 Along the lines above, encode all of the constructs of
-Chapter [More][plfa.More],
+Chapter [More]({{ site.baseurl }}/More/),
 save for primitive numbers, in the untyped lambda calculus.
 
 ```