Fixed left inverse in Isomorphism

Notes.md

@@ -8,6 +8,21 @@ permalink: /Notes/
 
 <https://analytics.google.com/analytics/web/>
 
+## Git commands
+
+Git commands to create a branch and pull request
+
+    git help <command>          -- get help on <command>
+    git branch                  -- list all branches
+    git branch <name>           -- create new local branch <name>
+    git checkout <name>         -- make <name> the current branch
+    git merge <name>            -- merge branch <name> into current branch 
+    git push origin <name>      -- make local branch <name> into remote
+    git rebase <base>           -- merge branch <base> into current branch
+
+On website, use pulldown menu to swith branch and then
+click "new pull request" button.
+
 ## Suggestion from Conor for Inference
 
 Conor McBride <conor.mcbride@strath.ac.uk>

README.md

@@ -171,7 +171,8 @@ configuration file at `~/.emacs`, if you have the mentioned fonts available:
 
 ## Markdown
 
-The book is written in [Kramdown Markdown](https://kramdown.gettalong.org/syntax.html).
+The book is written in
+[Kramdown Markdown](https://kramdown.gettalong.org/syntax.html).
 
 
 ## Travis Continuous Integration

src/plfa/Equality.lagda

@@ -348,7 +348,7 @@ an order that will make sense to the reader.
 
 The proof of monotonicity from
 Chapter [Relations][plfa.Relations]
-can be written in a more readable form by using an anologue of our
+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
 regard to inequality.  Rewrite both `+-monoˡ-≤` and `+-mono-≤`.
@@ -399,7 +399,7 @@ even-comm : ∀ (m n : ℕ)
 even-comm m n ev  rewrite +-comm n m  =  ev
 \end{code}
 Here `ev` ranges over evidence that `even (m + n)` holds, and we show
-that it is also provides evidence that `even (n + m)` holds.  In
+that it also provides evidence that `even (n + m)` holds.  In
 general, the keyword `rewrite` is followed by evidence of an
 equality, and that equality is used to rewrite the type of the
 goal and of any variable in scope.
@@ -452,8 +452,8 @@ here is a second proof that addition is commutative, relying on rewrites rather
 than chains of equalities:
 \begin{code}
 +-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
-+-comm′ zero    n  rewrite +-identity n            =  refl
-+-comm′ (suc m) n  rewrite +-suc n m | +-comm m n  =  refl
++-comm′ zero    n  rewrite +-identity n             =  refl
++-comm′ (suc m) n  rewrite +-suc n m | +-comm′ m n  =  refl
 \end{code}
 This is far more compact.  Among other things, whereas the previous
 proof required `cong suc (+-comm m n)` as the justification to invoke

src/plfa/Lists.lagda

@@ -778,7 +778,7 @@ operations associate to the left rather than the right.  For example:
 
 #### Exercise `foldr-monoid-foldl`
 
-Show that if `_⊕_` and `e` form a monoid, then `foldr _⊗_ e` and
+Show that if `_⊗_` and `e` form a monoid, then `foldr _⊗_ e` and
 `foldl _⊗_ e` always compute the same result.