From ae503a253493a848dc80942a0cc5f5393e268139 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= <marko@dimjasevic.net>
Date: Fri, 5 Jul 2019 22:45:40 +0200
Subject: [PATCH] TSPL: a few spelling error fixes in PUC Assignment 2

---
 tspl/PUC-Assignment2.lagda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/tspl/PUC-Assignment2.lagda b/tspl/PUC-Assignment2.lagda
index 131e32bc..e96dd34d 100644
--- a/tspl/PUC-Assignment2.lagda
+++ b/tspl/PUC-Assignment2.lagda
@@ -60,7 +60,7 @@ open import plfa.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
 
 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-≤`.
@@ -131,7 +131,7 @@ Show sum is commutative up to isomorphism.
 
 #### Exercise `⊎-assoc`
 
-Show sum is associative up to ismorphism. 
+Show sum is associative up to isomorphism.
 
 #### Exercise `⊥-identityˡ` (recommended)
 
@@ -415,7 +415,7 @@ data Tree (A B : Set) : Set where
   leaf : A → Tree A B
   node : Tree A B → B → Tree A B → Tree A B
 \end{code}
-Define a suitabve map operator over trees.
+Define a suitable map operator over trees.
 \begin{code}
 postulate
   map-Tree : ∀ {A B C D : Set}
@@ -460,7 +460,7 @@ postulate
 
 #### Exercise `map-is-fold-Tree`
 
-Demonstrate an anologue of `map-is-foldr` for the type of trees.
+Demonstrate an analogue of `map-is-foldr` for the type of trees.
 
 #### Exercise `sum-downFrom` (stretch)