small updates

Makefile

@@ -14,7 +14,7 @@ out/:
 	mkdir -p out/
 
 out/%.md: src/%.lagda | out/
-	agda2html --verbose --link-to-agda-stdlib --use-jekyll=out/ -i $< -o $@ 2>&1 \
+	agda2html --verbose --link-to-agda-stdlib --local-references --use-jekyll=out/ -i $< -o $@ 2>&1 \
 		| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
 	@sed -i '1 s|---|---\nsrc       : $(<)|' $@
 

README.md

@@ -32,6 +32,15 @@ The visible page appears at
 
     localhost:4000/<permalink>
 
+
+## Updates to agda2html
+
+Go to your clone of the agda2html repository, and run
+
+    $ git pull
+    $ stack install
+
+
 ## Unicode abbreviations
 
 
@@ -46,6 +55,7 @@ See
 [agda-input.el](https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194)
 for more details.
 
+
 ## How to use `agda-mode`
 
     ?            create hole
@@ -56,6 +66,7 @@ for more details.
 
 See [the emacs-mode docs](http://agda.readthedocs.io/en/latest/tools/emacs-mode.html) for more details.
 
+
 ## Markdown
 
 For an overview of the Markdown syntax, see
@@ -85,6 +96,7 @@ You can check this worked:
     nothing added to commit but untracked files present (use "git add" to track)
     bruichladdich$
 
+
 ## Analytics
 
 [Google Analytics](http://analytics.google.com/analytics/web/)

src/plfa/Acknowledgements.lagda

@@ -29,6 +29,7 @@ For pull requests:
 * Léo Gillot-Lamure
 * Zbigniew Stanasiuk 
 * Anish Tondwalkar
+* Spencer Whitt
 
 For answering questions on the Agda mailing list:
 * Guillaume Allais <guillaume.allais@ens-lyon.org>

src/plfa/Connectives.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "Connectives: Conjunction, disjunction, and implication"
 layout    : page
-prev      : /Isomorphisms/
+prev      : /Isomorphism/
 permalink : /Connectives/
 next      : /Negation/
 ---

src/plfa/Induction.lagda

@@ -586,7 +586,6 @@ Write out what is known about associativity of addition on each of the first fou
 days using a finite story of creation, as
 [earlier]({{ site.baseurl }}{% link out/plfa/Naturals.md %}#finite-creation).
 
-
 ## Associativity with rewrite
 
 There is more than one way to skin a cat.  Here is a second proof of

src/plfa/Naturals.lagda

@@ -603,8 +603,9 @@ 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.
+<!--
 We should call it frigging!
-
+-->
 
 ## The story of creation, revisited
 

src/plfa/Properties.lagda

@@ -1441,11 +1441,11 @@ false, give a counterexample.
 Suppose instead that we add a new term `foo` with the following
 reduction rules:
 
-  ------------------ β-foo₁
-  (λ x ⇒ ` x) —→ foo
+    ------------------ β-foo₁
+    (λ x ⇒ ` x) —→ foo
 
-  ----------- β-foo₂
-  foo —→ zero
+    ----------- β-foo₂
+    foo —→ zero
 
 Which of the following properties remain true in
 the presence of this rule?  For each one, write either