Fixing two problems in chapter Inference (#1073)

* Update Inference.lagda.md

* Update Inference.lagda.md

Author: hafniz

src/plfa/part2/Inference.lagda.md

@@ -173,8 +173,8 @@ judgment returns `A` as the synthesized type of the term as a whole,
 as well as using it as the inherited type for `M`.
 
 The term form `M ↓ A` represents the only place terms need to be
-decorated with types.  It only appears when switching from synthesis
-to inheritance, that is, when a term that _deconstructs_ a value of a
+decorated with types.  It only appears when switching from inheritance
+to synthesis, that is, when a term that _deconstructs_ a value of a
 type contains as its main term a term that _constructs_ a value of a
 type, in other words, a place where a `β`-reduction will occur.
 Typically, we will find that decorations are only required on top
@@ -185,15 +185,15 @@ We can extract the grammar for terms from the above:
     L⁺, M⁺, N⁺ ::=                      terms with synthesized type
       x                                   variable
       L⁺ · M⁻                             application
-      M⁻ ↓ A                              switch to inherited
+      M⁻ ↓ A                              switch from inherited
 
     L⁻, M⁻, N⁻ ::=                      terms with inherited type
       ƛ x ⇒ N⁻                            abstraction
       `zero                               zero
       `suc M⁻                             successor
       case L⁺ [zero⇒ M⁻ |suc x ⇒ N⁻ ]     case
       μ x ⇒ N⁻                            fixpoint
-      M⁺ ↑                                switch to synthesized
+      M⁺ ↑                                switch from synthesized
 
 We will formalise the above shortly.
 
@@ -217,9 +217,9 @@ Similarly, given context `Γ`, inherited term `M`, and type `A`, we
 must decide whether `Γ ⊢ M ↓ A` holds, or its negation.
 
 Our proof is constructive. In the synthesised case, it will either
-deliver a pair of a type `A` and evidence that `Γ ⊢ M ↓ A`, or a function
+deliver a pair of a type `A` and evidence that `Γ ⊢ M ↑ A`, or a function
 that given such a pair produces evidence of a contradiction. In the inherited
-case, it will either deliver evidence that `Γ ⊢ M ↑ A`, or a function
+case, it will either deliver evidence that `Γ ⊢ M ↓ A`, or a function
 that given such evidence produces evidence of a contradiction.
 The positive case is referred to as _soundness_ --- synthesis and inheritance
 succeed only if the corresponding relation holds.  The negative case is