Typo fixes

Fixes #117 and #128, with credit

examples/Examples/Intro.lean

@@ -1674,7 +1674,7 @@ end expect
 
 
 bookExample type {{{ swapLambda }}}
-  fun (point : Point) => { x := point.y, y := point.x : Point}
+  fun (point : Point) => { x := point.y, y := point.x : Point }
   ===>
   (Point → Point)
 end bookExample

functional-programming-lean/src/acknowledgments.md

@@ -12,5 +12,5 @@ An extra day of work each week has not been easy for my family—thank you for y
 The online community surrounding Lean provided enthusiastic support for the project, both technical and emotional.
 In particular, Sebastian Ullrich provided key help when I was learning Lean's metaprogramming system in order to write the supporting code that allowed the text of error messages to be both checked in CI and easily included in the book itself.
 Within hours of posting a new revision, excited readers would be finding mistakes, providing suggestions, and showering me with kindness.
-In particular, I'd like to thank Arien Malec, Asta Halkjær From, Bulhwi Cha, Daniel Fabian, Evgenia Karunus, eyelash, Floris van Doorn, František Silváši, Henrik Böving, Ian Young, Jeremy Salwen, Jireh Loreaux, Kevin Buzzard, Mac Malone, Malcolm Langfield, Mario Carneiro, Newell Jensen, Patrick Massot, Paul Chisholm, Tomas Puverle, Yaël Dillies, and Zhiyuan Bao for their many suggestions, both stylistic and technical.
+In particular, I'd like to thank Arien Malec, Asta Halkjær From, Bulhwi Cha, Daniel Fabian, Evgenia Karunus, eyelash, Floris van Doorn, František Silváši, Henrik Böving, Ian Young, Jeremy Salwen, Jireh Loreaux, Kevin Buzzard, Mac Malone, Malcolm Langfield, Mario Carneiro, Newell Jensen, Patrick Massot, Paul Chisholm, Pietro Monticone, Tomas Puverle, Yaël Dillies, Zhiyuan Bao, and Zyad Hassan for their many suggestions, both stylistic and technical.
 

functional-programming-lean/src/dependent-types/summary.md

@@ -55,7 +55,7 @@ Avoiding these slowdowns for complicated programs can require specialized techni
 
 ## Definitional and Propositional Equality
 
-Lean's type checker must, from time to time, check whether two types should be considered interchangable.
+Lean's type checker must, from time to time, check whether two types should be considered interchangeable.
 Because types can contain arbitrary programs, it must therefore be able to check arbitrary programs for equality.
 However, there is no efficient algorithm to check arbitrary programs for fully-general mathematical equality.
 To work around this, Lean contains two notions of equality:

functional-programming-lean/src/functor-applicative-monad/complete.md

@@ -128,5 +128,5 @@ From the perspective of API boundaries, any type with a `Monad` instance gets in
 
 ## Exercises
 
- 1. Understand the default implementations of `map`, `seq`, `seqLeft`, and `seqRight` in `Monad` by working through examples such as `Option` and `Except`. In other words, subsitute their definitions for `bind` and `pure` into the default definitions, and simplify them to recover the versions `map`, `seq`, `seqLeft`, and `seqRight` that would be written by hand.
+ 1. Understand the default implementations of `map`, `seq`, `seqLeft`, and `seqRight` in `Monad` by working through examples such as `Option` and `Except`. In other words, substitute their definitions for `bind` and `pure` into the default definitions, and simplify them to recover the versions `map`, `seq`, `seqLeft`, and `seqRight` that would be written by hand.
  2. On paper or in a text file, prove to yourself that the default implementations of `map` and `seq` satisfy the contracts for `Functor` and `Applicative`. In this argument, you're allowed to use the rules from the `Monad` contract as well as ordinary expression evaluation.

functional-programming-lean/src/monads.md

@@ -1,7 +1,7 @@
 # Monads
 
 In C# and Kotlin, the `?.` operator is a way to look up a property or call a method on a potentially-null value.
-If the reciever is `null`, the whole expression is null.
+If the receiver is `null`, the whole expression is null.
 Otherwise, the underlying non-`null` value receives the call.
 Uses of `?.` can be chained, in which case the first `null` result terminates the chain of lookups.
 Chaining null-checks like this is much more convenient than writing and maintaining deeply nested `if`s.