diff --git a/hs/agda-count b/hs/agda-count
index d17f98f7..07445ac5 100755
Binary files a/hs/agda-count and b/hs/agda-count differ
diff --git a/hs/config.txt b/hs/config.txt
index b7d0b5ee..dbd1cf37 100644
--- a/hs/config.txt
+++ b/hs/config.txt
@@ -15,6 +15,7 @@ Lambda
 Properties
 DeBruijn
 More
+Bisimulation
 Inference
 Untyped
 --
diff --git a/src/plfa/Fonts.lagda b/src/plfa/Fonts.lagda
index dcb1b710..3059959e 100644
--- a/src/plfa/Fonts.lagda
+++ b/src/plfa/Fonts.lagda
@@ -37,6 +37,7 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ|
 ≡≡≢≢|
 ≃≃≲≲|
 ≟≟≐≐|
+∸∸^^|
 ⟨⟨⟩⟩|
 ⌊⌊⌋⌋|
 ⌈⌈⌉⌉|
@@ -46,6 +47,7 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ|
 ∈∈∋∋|
 ⊢⊢⊣⊣|
 ∷∷∷∷|
+∎∎∎∎|
 ⦂⦂⦂⦂|
 ----|
 -}
diff --git a/src/plfa/Naturals.lagda b/src/plfa/Naturals.lagda
index c492cd8a..9dfc20ee 100644
--- a/src/plfa/Naturals.lagda
+++ b/src/plfa/Naturals.lagda
@@ -874,7 +874,7 @@ This chapter uses the following unicode.
     ℕ  U+2115  DOUBLE-STRUCK CAPITAL N (\bN)
     →  U+2192  RIGHTWARDS ARROW (\to, \r)
     ∸  U+2238  DOT MINUS (\.-)
-    ≡  U+2261  IDENTICAL TO (\==)  =
+    ≡  U+2261  IDENTICAL TO (\==)
     ⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET (\<)
     ⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
     ∎  U+220E  END OF PROOF (\qed)
@@ -887,7 +887,7 @@ The command `\r` gives access to a wide variety of rightward arrows.
 After typing `\r`, one can access the many available arrows by using
 the left, right, up, and down keys to navigate.  The command remembers
 where you navigated to the last time, and starts with the same
-character next time.
+character next time.  The command `\l` works similarly for left arrows.
 
 In place of left, right, up, and down keys, one may also use control characters.
 
@@ -897,4 +897,4 @@ In place of left, right, up, and down keys, one may also use control characters.
     ^N  down (dowN)
 
 We write `^B` to stand for control-B, and similarly.  One can also navigate
-left and write by typing the digits that appear in the displayed list.
+left and right by typing the digits that appear in the displayed list.
diff --git a/src/plfa/Statistics.lagda b/src/plfa/Statistics.lagda
index b5e9e85c..780b53da 100644
--- a/src/plfa/Statistics.lagda
+++ b/src/plfa/Statistics.lagda
@@ -9,7 +9,7 @@ Total number of lines and number of lines of Agda code in each chapter
 
                                 total   code
                                 -----   ----
-    Preface                       99       1
+    Preface                       92       0
 
     Naturals                     900      86
     Induction                    770     107
@@ -22,13 +22,14 @@ Total number of lines and number of lines of Agda code in each chapter
     Lists                        893     412
     Decidable                    566     170
 
-    Lambda                      1300     386
-    Properties                  1533     724
-    DeBruijn                    1363     627
-    More                         603     524
+    Lambda                      1304     389
+    Properties                  1539     568
+    DeBruijn                    1363     635
+    More                         675     570
+    Bisimulation                 151     110
     Inference                    431     350
     Untyped                      362     281
 
-    Acknowledgements              46       1
-    Fonts                         62      44
-    Statistics                    38       1
+    Acknowledgements              44       0
+    Fonts                         78      59
+    Statistics                    34       0
diff --git a/src/plfa/Untyped.lagda b/src/plfa/Untyped.lagda
index 7cd39ea5..b5fe7abd 100644
--- a/src/plfa/Untyped.lagda
+++ b/src/plfa/Untyped.lagda
@@ -136,9 +136,9 @@ data Normal  : ∀ {n} → Term n → Set
 data Neutral where
 
   ⌊_⌋  : ∀ {n}
-    → (k : Var n)
+    → (x : Var n)
       -------------
-    → Neutral ⌊ k ⌋
+    → Neutral ⌊ x ⌋
 
   _·_  : ∀ {n} {L : Term n} {M : Term n}
     → Neutral L
@@ -155,6 +155,7 @@ data Normal where
 
   ⌈_⌉ : ∀ {n} {M : Term n}
     → Neutral M
+      ---------
     → Normal M
 \end{code}