merge

_includes/script.html

@@ -1,6 +1,11 @@
 <!-- Import jQuery -->
 <script type="text/javascript" src="{{ "/assets/jquery.js" | prepend: site.baseurl }}"></script>
 
+<script src="https://cdnjs.cloudflare.com/ajax/libs/anchor-js/4.2.2/anchor.min.js" integrity="sha256-E4RlfxwyJVmkkk0szw7LYJxuPlp6evtPSBDlWHsYYL8=" crossorigin="anonymous"></script>
+<script type="text/javascript">
+  anchors.add();
+</script>
+
 <script type="text/javascript">
 
  // Makes sandwhich menu works

src/plfa/part1/Induction.lagda.md

@@ -656,8 +656,8 @@ time we are concerned with judgments asserting associativity:
 
 Now, we apply the rules to all the judgments we know about.  The base
 case tells us that `(zero + n) + p ≡ zero + (n + p)` for every natural
-`n` and `p`.  The inductive case tells us that if `(m + n) + p ≡ m +
+`n` and `p`.  The inductive case tells us that if 
-(n + p)` (on the day before today) then
+`(m + n) + p ≡ m + (n + p)` (on the day before today) then
 `(suc m + n) + p ≡ suc m + (n + p)` (today).
 We didn't know any judgments about associativity before today, so that
 rule doesn't give us any new judgments:

src/plfa/part1/Naturals.lagda.md

@@ -239,11 +239,10 @@ Including the line
 ```
 tells Agda that `ℕ` corresponds to the natural numbers, and hence one
 is permitted to type `0` as shorthand for `zero`, `1` as shorthand for
-`suc zero`, `2` as shorthand for `suc (suc zero)`, and so on.  The
+`suc zero`, `2` as shorthand for `suc (suc zero)`, and so on. The pragma
-declaration is not permitted unless the type given has exactly two
+must be given a previously declared type (in this case `ℕ`) with
-constructors, one with no arguments (corresponding to zero) and
+precisely two constructors, one with no arguments (in this case `zero`),
-one with a single argument of the same type given in the pragma
+and one with a single argument of the given type (in this case `suc`).
-(corresponding to successor).
 
 As well as enabling the above shorthand, the pragma also enables a
 more efficient internal representation of naturals using the Haskell
@@ -628,7 +627,7 @@ since the same idea was previously proposed by Moses Schönfinkel in
 the 1920's.  I was told a joke: "It should be called schönfinkeling,
 but currying is tastier". Only later did I learn that the explanation
 of the misattribution was itself a misattribution.  The idea actually
-appears in the _Begriffschrift_ of Gottlob Frege, published in 1879.
+appears in the _Begriffsschrift_ of Gottlob Frege, published in 1879.
 
 ## The story of creation, revisited
 

src/plfa/part1/Quantifiers.lagda.md

@@ -473,15 +473,11 @@ for `Can b`.
     
     ≡Can : ∀{b : Bin} (cb : Can b) (cb' : Can b) → cb ≡ cb'
 
-The proof of `to∘from` is tricky. We recommend proving the following lemma
+Many of the alternatives for proving `to∘from` turn out to be tricky.
+However, the proof can be straightforward if you use the following lemma,
+which is a corollary of `≡Can`.
 
-    to∘from-aux : ∀ (b : Bin) (cb : Can b) → to (from b) ≡ b
+    proj₁≡→Can≡ : {cb cb′ : ∃[ b ](Can b)} → proj₁ cb ≡ proj₁ cb′ → cb ≡ cb′
-                → _≡_ {_} {∃[ b ](Can b)} ⟨ to (from b) , canon-to (from b) ⟩ ⟨ b , cb ⟩
-
-You cannot immediately use `≡Can` to equate `canon-to (from b)` and
-`cb` because they have different types: `Can (to (from b))` and `Can b`
-respectively.  You must first get their types to be equal, which
-can be done by changing the type of `cb` using `rewrite`.
 
 ```
 -- Your code goes here