moved to plfa, small fixes

src/plfa/Acknowledgements.lagda

@@ -4,21 +4,19 @@ layout    : page
 permalink : /Acknowledgements/
 ---
 
-\begin{code}
-module plta.Acknowledgements where
-\end{code}
+Thank you to:
+* The inventors of Agda, for a new playground.
+* The authors of Software Foundations, for inspiration.
 
-Thank you to the following.
+A special thank you, for inventing ideas on which
+this book is based, and for hand-holding.
+* Conor McBride
+* James McKinna
+* Ulf Norell
+* Andreas Abel
 
-To the inventors of Agda, for giving us a new playground.
-
-To the authors of Software Foundations, for inspiration.
-
-To Conor McBride and James McKinna, for cool ideas and handholding.
-
-To Andreas Abel and Ulf Norell, ditto.
-
-To David Darais, for showing us how much more compact it is to avoid raw terms.
+For a note showing how much more compact it is to avoid raw terms.
+* David Darais
 
 For pull requests.
 * Vikraman Choudhury

src/plfa/Bisimulation.lagda

@@ -5,7 +5,7 @@ permalink : /Bisimulation/
 ---
 
 \begin{code}
-module plta.Bisimulation where
+module plfa.Bisimulation where
 \end{code}
 
 
@@ -21,7 +21,7 @@ open import Data.Unit using (⊤; tt)
 open import Function using (_∘_)
 open import Function.Equivalence using (_⇔_; equivalence)
 open import Relation.Nullary using (¬_; Dec; yes; no)
-open import plta.More
+open import plfa.More
 \end{code}
 
 

src/plfa/Connectives.lagda

@@ -28,8 +28,8 @@ open Eq.≡-Reasoning
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
 open import Data.Nat.Properties using (+-suc)
 open import Function using (_∘_)
-open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
-open plta.Isomorphism.≃-Reasoning
+open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
+open plfa.Isomorphism.≃-Reasoning
 \end{code}
 
 
@@ -807,9 +807,9 @@ The former makes it convenient to make 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 `[_,_]` and `[_,_,_]` to construct
 lists of two or three elements in
-Chapter [Lists]({{ site.baseurl }}{% link out/plta/Lists.md %})
+Chapter [Lists]({{ site.baseurl }}{% link out/plfa/Lists.md %})
 or `Γ , A` to extend environments in
-Chapter [DeBruijn]({{ site.baseurl }}{% link out/plta/DeBruijn.md %}).
+Chapter [DeBruijn]({{ site.baseurl }}{% link out/plfa/DeBruijn.md %}).
 
 
 

src/plfa/DeBruijn.lagda

@@ -54,10 +54,10 @@ And here is its corresponding type derivation:
                ∋z = Z
 
 (These are both taken from Chapter
-[Lambda]({{ site.baseurl }}{% link out/plta/Lambda.md %})
+[Lambda]({{ site.baseurl }}{% link out/plfa/Lambda.md %})
 and you can see the corresponding derivation tree written out
 in full
-[here]({{ site.baseurl }}{% link out/plta/Lambda.md %}/#derivation).)
+[here]({{ site.baseurl }}{% link out/plfa/Lambda.md %}/#derivation).)
 The two definitions are in close correspondence, where
 
   * `` `_ `` corresponds to `Ax`
@@ -111,7 +111,7 @@ 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]({{ site.baseurl }}{% link
-out/plta/Untyped.md %}, we will terms that are not typed with
+out/plfa/Untyped.md %}, we will terms that are not typed with
 De Bruijn indices are inherently scoped.
 
 
@@ -436,7 +436,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]({{ site.baseurl }}{% link out/plta/Lambda.md %}/#impossible).
+[here]({{ site.baseurl }}{% link out/plfa/Lambda.md %}/#impossible).
 
 Given the above, we can convert a natural to a corresponding
 De Bruijn indice, looking up its type in the context.
@@ -465,9 +465,9 @@ _ = ƛ ƛ (# 1 · (# 1 · # 0))
 ### Test examples
 
 We repeat the test examples from
-Chapter [Lambda]({{ site.baseurl }}{% link out/plta/Lambda.md %}).
+Chapter [Lambda]({{ site.baseurl }}{% link out/plfa/Lambda.md %}).
 You can find the 
-[here]({{ site.baseurl }}{% link out/plta/Lambda.md %}/#derivation)
+[here]({{ site.baseurl }}{% link out/plfa/Lambda.md %}/#derivation)
 for comparison.
 
 First, computing two plus two on naturals.
@@ -804,7 +804,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]({{ site.baseurl }}{% link out/plta/Lists.md %})).
+[Lists]({{ site.baseurl }}{% link out/plfa/Lists.md %})).
 
 ### Reduction step
 

src/plfa/Decidable.lagda

@@ -33,7 +33,7 @@ open import Function using (_∘_)
 
 ## Evidence vs Computation
 
-Recall that Chapter [Relations]({{ site.baseurl }}{% link out/plta/Relations.md %})
+Recall that Chapter [Relations]({{ site.baseurl }}{% link out/plfa/Relations.md %})
 defined comparison an inductive datatype, which provides *evidence* that one number
 is less than or equal to another.
 \begin{code}
@@ -496,7 +496,7 @@ on which matches; but either is equally valid.
 
 ## Decidability of All
 
-Recall that in Chapter [Lists]({{ site.baseurl }}{% link out/plta/Lists.md %}#All)
+Recall that in Chapter [Lists]({{ site.baseurl }}{% link out/plfa/Lists.md %}#All)
 we defined a predicate `All P` that holds if a given predicate is satisfied by every element of a list.
 \begin{code}
 data All {A : Set} (P : A → Set) : List A → Set where
@@ -513,7 +513,7 @@ all p  =  foldr _∧_ true ∘ map p
 \end{code}
 The function can be written in a particularly compact style by
 using the higher-order functions `map` and `foldr` as defined in
-the sections on [Map]({{ site.baseurl }}{% link out/plta/Lists.md %}#Map) and [Fold]({{ site.baseurl }}{% link out/plta/Lists.md %}#Fold).
+the sections on [Map]({{ site.baseurl }}{% link out/plfa/Lists.md %}#Map) and [Fold]({{ site.baseurl }}{% link out/plfa/Lists.md %}#Fold).
 
 As one would hope, if we replace booleans by decidables there is again
 an analogue of `All`.  First, return to the notion of a predicate `P` as

src/plfa/Induction.lagda

@@ -538,7 +538,7 @@ which is left as an exercise for the reader.
 
 Write out what is known about associativity on each of the first four
 days using a finite story of creation, as
-[earlier]({{ site.baseurl }}{% link out/plta/Naturals.md %}#finite-creation).
+[earlier]({{ site.baseurl }}{% link out/plfa/Naturals.md %}#finite-creation).
 
 
 ## Associativity with rewrite

src/plfa/Inference.lagda

@@ -25,7 +25,7 @@ open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Function using (_∘_)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Nullary.Negation using (¬?)
-open import plta.DeBruijn as DB using (Type; `ℕ; _⇒_)
+open import plfa.DeBruijn as DB using (Type; `ℕ; _⇒_)
 
 pattern [_]       w        =  w ∷ []
 pattern [_,_]     w x      =  w ∷ x ∷ []
@@ -56,9 +56,9 @@ These should get imported from Typed (or Fresh, or Raw).
 Id : Set
 Id = String
 
-data Ctx : Set where
-  ∅      : Ctx
-  _,_⦂_ : Ctx → Id → Type → Ctx
+data Context : Set where
+  ∅      : Context
+  _,_⦂_ : Context → Id → Type → Context
 \end{code}
 
 Terms that synthesize `Term⁺` and inherit `Term⁻` their types.
@@ -111,7 +111,7 @@ sucᶜ = ƛ "x" ⇒ `suc (` "x" ↑)
 ## Bidirectional type checking
 
 \begin{code}
-data _∋_⦂_ : Ctx → Id → Type → Set where
+data _∋_⦂_ : Context → Id → Type → Set where
 
   Z : ∀ {Γ x A}
       --------------------
@@ -123,8 +123,8 @@ data _∋_⦂_ : Ctx → Id → Type → Set where
       --------------------
     → Γ , x ⦂ A ∋ w ⦂ B
 
-data _⊢_↑_ : Ctx → Term⁺ → Type → Set
-data _⊢_↓_ : Ctx → Term⁻ → Type → Set
+data _⊢_↑_ : Context → Term⁺ → Type → Set
+data _⊢_↓_ : Context → Term⁻ → Type → Set
 
 data _⊢_↑_ where
 
@@ -212,7 +212,7 @@ _≟Tp_ : (A B : Type) → Dec (A ≡ B)
 ## Lookup type of a variable in the context
 
 \begin{code}
-lookup : ∀ (Γ : Ctx) (x : Id) → TC (∃[ A ](Γ ∋ x ⦂ A))
+lookup : ∀ (Γ : Context) (x : Id) → TC (∃[ A ](Γ ∋ x ⦂ A))
 lookup ∅ x  =
   error⁺ "variable not bound" (` x) []
 lookup (Γ , x ⦂ A) w with w ≟ x
@@ -226,8 +226,8 @@ lookup (Γ , x ⦂ A) w with w ≟ x
 ## Synthesize and inherit types
 
 \begin{code}
-synthesize : ∀ (Γ : Ctx) (M : Term⁺) → TC (∃[ A ](Γ ⊢ M ↑ A))
-inherit : ∀ (Γ : Ctx) (M : Term⁻) (A : Type) → TC (Γ ⊢ M ↓ A)
+synthesize : ∀ (Γ : Context) (M : Term⁺) → TC (∃[ A ](Γ ⊢ M ↑ A))
+inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type) → TC (Γ ⊢ M ↓ A)
 
 synthesize Γ (` x) =
   do ⟨ A , ⊢x ⟩ ← lookup Γ x
@@ -397,7 +397,7 @@ _ = refl
 ## Erasure
 
 \begin{code}
-∥_∥Γ : Ctx → DB.Ctx
+∥_∥Γ : Context → DB.Context
 ∥ ∅ ∥Γ = DB.∅
 ∥ Γ , x ⦂ A ∥Γ = ∥ Γ ∥Γ DB., A
 
@@ -415,7 +415,7 @@ _ = refl
 ∥ ⊢ƛ ⊢N ∥⁻ =  DB.ƛ ∥ ⊢N ∥⁻
 ∥ ⊢zero ∥⁻ =  DB.`zero
 ∥ ⊢suc ⊢M ∥⁻ =  DB.`suc ∥ ⊢M ∥⁻
-∥ ⊢case ⊢L ⊢M ⊢N ∥⁻ =  DB.`case ∥ ⊢L ∥⁺ ∥ ⊢M ∥⁻ ∥ ⊢N ∥⁻
+∥ ⊢case ⊢L ⊢M ⊢N ∥⁻ =  DB.case ∥ ⊢L ∥⁺ ∥ ⊢M ∥⁻ ∥ ⊢N ∥⁻
 ∥ ⊢μ ⊢M ∥⁻ =  DB.μ ∥ ⊢M ∥⁻
 ∥ ⊢↑ ⊢M refl ∥⁻ =  ∥ ⊢M ∥⁺
 \end{code}

src/plfa/Isomorphism.lagda

@@ -87,7 +87,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 functions.  It is the
 converse of `cong-app`, as introduced
-[earlier]({{ site.baseurl }}{% link out/plta/Equality.md %}/#cong).
+[earlier]({{ site.baseurl }}{% link out/plfa/Equality.md %}/#cong).
 
 Agda does not presume extensionality, but we can postulate that it holds.
 \begin{code}
@@ -99,7 +99,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]({{ site.baseurl }}{% link out/plta/Naturals.md %})
+Chapter [Naturals]({{ site.baseurl }}{% link out/plfa/Naturals.md %})
 and one where it is defined the other way around.
 \begin{code}
 _+′_ : ℕ → ℕ → ℕ

src/plfa/Lambda.lagda

@@ -32,7 +32,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]({{ site.baseurl }}{% link out/plta/Properties.md %})
+[Properties]({{ site.baseurl }}{% link out/plfa/Properties.md %})
 proves its main properties, including
 progress and preservation.  Following chapters will look at a number
 of variants of lambda calculus.
@@ -40,7 +40,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]({{ site.baseurl }}{% link out/plta/DeBruijn.md %}),
+Chapter [DeBruijn]({{ site.baseurl }}{% link out/plfa/DeBruijn.md %}),
 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.
@@ -148,7 +148,7 @@ plus =  μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
 \end{code}
 The recursive definition of addition is similar to our original
 definition of `_+_` for naturals, as given in
-Chapter [Naturals]({{ site.baseurl }}{% link out/plta/Naturals.md %}#plus).
+Chapter [Naturals]({{ site.baseurl }}{% link out/plfa/Naturals.md %}#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
@@ -333,7 +333,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]({{ site.baseurl }}{% link out/plta/Untyped.md %}).
+Chapter [Untyped]({{ site.baseurl }}{% link out/plfa/Untyped.md %}).
 
 
 ## Substitution
@@ -613,7 +613,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
-Chapter [Equality]({{ site.baseurl }}{% link out/plta/Equality.md %}).
+Chapter [Equality]({{ site.baseurl }}{% link out/plfa/Equality.md %}).
 \begin{code}
 infix  2 _—↠_
 infix  1 begin_
@@ -1084,7 +1084,7 @@ with the empty type `⊥`.  If we use `C `N to normalise the term
 
 Agda will return an answer warning us that the impossible has occurred:
 
-    ⊥-elim (.plta.Lambda.impossible "a" "a" refl)
+    ⊥-elim (.plfa.Lambda.impossible "a" "a" refl)
 
 While postulating the impossible is a useful technique, it must be
 used with care, since such postulation could allow us to provide
@@ -1218,7 +1218,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]({{ site.baseurl }}{% link out/plta/DeBruijn.md %})
+Chapter [Inference]({{ site.baseurl }}{% link out/plfa/DeBruijn.md %})
 will show how to use Agda to compute type derivations directly.
 
 

src/plfa/Lists.lagda

@@ -25,7 +25,7 @@ open import Relation.Nullary using (¬_)
 open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
 open import Function using (_∘_)
 open import Level using (Level)
-open import plta.Isomorphism using (_≃_)
+open import plfa.Isomorphism using (_≃_)
 \end{code}
 
 
@@ -854,7 +854,7 @@ _∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂}
 (g ∘′ f) x  =  g (f x)
 \end{code}
 
-[unipoly]: {{ site.baseurl }}{% link out/plta/Equality.md %}#unipoly
+[unipoly]: {{ site.baseurl }}{% link out/plfa/Equality.md %}#unipoly
 
 Show that `Any` and `All` satisfy a version of De Morgan's Law.
 \begin{code}

src/plfa/Modules.lagda

@@ -29,7 +29,7 @@ open import Data.Maybe using (Maybe; just; nothing)
 open import Data.List using (List; []; _∷_; _++_; map; foldr; downFrom)
 open import Data.List.All using (All; []; _∷_)
 open import Data.List.Any using (Any; here; there)
-open import plta.Isomorphism using (_≃_; extensionality)
+open import plfa.Isomorphism using (_≃_; extensionality)
 \end{code}
 
 

src/plfa/Naturals.lagda

@@ -269,7 +269,7 @@ specifies operators to support reasoning about equivalence, and adds
 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 all these as givens for now,
-but will see how they are defined in Chapter [Equality]({{ site.baseurl }}{% link out/plta/Equality.md %}).
+but will see how they are defined in Chapter [Equality]({{ site.baseurl }}{% link out/plfa/Equality.md %}).
 
 Agda uses underbars to indicate where terms appear in infix or mixfix
 operators. Thus, `_≡_` and `_≡⟨⟩_` are infix (each operator is written

src/plfa/Negation.lagda

@@ -20,7 +20,7 @@ open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
 open import Function using (_∘_)
-open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
+open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
 \end{code}
 
 
@@ -142,13 +142,13 @@ when `A` is anything other than `⊥` itself.
 
 ### Exercise (`≢`, `<-irrerflexive`)
 
-Using negation, show that [strict inequality]({{ site.baseurl }}{% link out/plta/Relations.md %}/#strict-inequality)
+Using negation, show that [strict inequality]({{ site.baseurl }}{% link out/plfa/Relations.md %}/#strict-inequality)
 is irreflexive, that is, `n < n` holds for no `n`.
 
 
 ### Exercise (`trichotomy`)
 
-Show that strict inequality satisfies [trichotomy]({{ site.baseurl }}{% link out/plta/Relations.md %}/#trichotomy),
+Show that strict inequality satisfies [trichotomy]({{ site.baseurl }}{% link out/plfa/Relations.md %}/#trichotomy),
 that is, for any naturals `m` and `n` exactly one of the following holds:
 
 * `m < n`

src/plfa/Preface.lagda

@@ -12,14 +12,11 @@ either the proof of the proposition or as a programme of the
 corresponding type.  Further still, simplification of proofs
 corresponds to evaluation of programs.
 
-The title of this book also has two readings.  "Code the
-Infinite" may be taken as a declarative — code is everything — or as
-an imperative — write code to capture an infinite realm.  Further, the
-subtitle may be parsed as "(Programming Language Foundations) in Agda"
-or "Programming (Language Foundations) in Agda" — the specifications
-we will write in the proof assistant Agda both describe programming
-languages and are themselves programmes.
-
+The title of this book also has two readings.  It may be parsed as
+"(Programming Language Foundations) in Agda" or "Programming (Language
+Foundations) in Agda" — the specifications we will write in the proof
+assistant Agda both describe programming languages and are themselves
+programmes.
 
 ## Personal remarks
 

src/plfa/Properties.lagda

@@ -33,8 +33,8 @@ open import Data.Product
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Function using (_∘_)
-open import plta.Isomorphism
-open import plta.Lambda
+open import plfa.Isomorphism
+open import plfa.Lambda
 \end{code}
 
 

src/plfa/Quantifiers.lagda

@@ -22,7 +22,7 @@ open import Relation.Nullary using (¬_)
 open import Function using (_∘_)
 open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
+open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
 \end{code}
 
 
@@ -83,7 +83,7 @@ Show that universals distribute over conjunction.
 ∀-Distrib-× = ∀ {A : Set} {B C : A → Set} →
   (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
 \end{code}
-Compare this with the result (`→-distrib-×`) in Chapter [Connectives]({{ site.baseurl }}{% link out/plta/Connectives.md %}).
+Compare this with the result (`→-distrib-×`) in Chapter [Connectives]({{ site.baseurl }}{% link out/plfa/Connectives.md %}).
 
 ### Exercise (`⊎∀-implies-∀⊎`)
 
@@ -209,7 +209,7 @@ 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][implication].
 
-[implication]: {{ site.baseurl }}{% link out/plta/Connectives.md %}/#implication
+[implication]: {{ site.baseurl }}{% link out/plfa/Connectives.md %}/#implication
 
 ### Exercise (`∃-distrib-⊎`)
 
@@ -231,7 +231,7 @@ Does the converse hold? If so, prove; if not, explain why.
 
 ## An existential example
 
-Recall the definitions of `even` and `odd` from Chapter [Relations]({{ site.baseurl }}{% link out/plta/Relations.md %}).
+Recall the definitions of `even` and `odd` from Chapter [Relations]({{ site.baseurl }}{% link out/plfa/Relations.md %}).
 \begin{code}
 data even : ℕ → Set
 data odd  : ℕ → Set

src/plfa/Relations.lagda

@@ -128,7 +128,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]({{ site.baseurl }}{% link out/plta/Decidable.md %}).
+will return to this point in Chapter [Decidable]({{ site.baseurl }}{% link out/plfa/Decidable.md %}).
 
 
 ## Properties of ordering relations
@@ -418,7 +418,7 @@ transitivity proves `m + p ≤ n + q`, as was to be shown.
 
 The proof of monotonicity (and the associated lemmas) can be written
 in a more readable form by using an anologue of our notation for
-`≡-reasoning`.  Read ahead to chapter [Equality]({{ site.baseurl }}{% link out/plta/Equality.md %}) to
+`≡-reasoning`.  Read ahead to chapter [Equality]({{ site.baseurl }}{% link out/plfa/Equality.md %}) to
 see how `≡-reasoning` is defined, define `≤-reasoning` analogously,
 and use it to write out an alternative proof that addition is
 monotonic with regard to inequality.
@@ -448,7 +448,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 the chapter that introduces [negation]({{ site.baseurl }}{% link out/plta/Negation.md %}).
+to the chapter that introduces [negation]({{ site.baseurl }}{% link out/plfa/Negation.md %}).
 
 It is straightforward to show that `suc m ≤ n` implies `m < n`,
 and conversely.  One can then give an alternative derivation of the
@@ -469,7 +469,7 @@ the sense that for any `m` and `n` that one of the following holds:
 This only involves two relations, as we 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 [negation]({{ site.baseurl }}{% link out/plta/Negation.md %}) is introduced.)
+are exclusive after [negation]({{ site.baseurl }}{% link out/plfa/Negation.md %}) is introduced.)
 
 ### Exercise (`+-mono-<`)
 
@@ -591,7 +591,7 @@ import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
                                   +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
 \end{code}
 In the standard library, `≤-total` is formalised in terms of
-disjunction (which we define in Chapter [Connectives]({{ site.baseurl }}{% link out/plta/Connectives.md %})),
+disjunction (which we define in Chapter [Connectives]({{ site.baseurl }}{% link out/plfa/Connectives.md %})),
 and `+-monoʳ-≤`, `+-monoˡ-≤`, `+-mono-≤` are proved differently than here
 as well as taking as implicit arguments that here are explicit.