diff --git a/content/blog/10_compiler_polymorphism.md b/content/blog/10_compiler_polymorphism.md
index 2179952..72d60ea 100644
--- a/content/blog/10_compiler_polymorphism.md
+++ b/content/blog/10_compiler_polymorphism.md
@@ -37,11 +37,11 @@ This is because, for this to work, both of the following would need to hold (bor
 some of our notation from the [typechecking]({{< relref "03_compiler_typechecking.md" >}}) post):
 
 {{< latex >}}
-\text{if} : \text{Int} \rightarrow \text{Int}
+\text{if} : \text{Bool} \rightarrow \text{Int} \rightarrow \text{Int} \rightarrow \text{Int}
 {{< /latex >}}
 
 {{< latex >}}
-\text{if} : \text{Bool} \rightarrow \text{Bool}
+\text{if} : \text{Bool} \rightarrow \text{Bool} \rightarrow \text{Bool} \rightarrow \text{Bool}
 {{< /latex >}}
 
 But using our rules so far, such a thing is impossible, since there is no way for
@@ -70,7 +70,7 @@ Rule|Name and Description
 \frac
     {\Gamma, x:\tau \vdash e : \tau'}
     {\Gamma \vdash \lambda x.e : \tau \rightarrow \tau'}
-{{< /latex >}}| __Abs__: If the body \\(e\\) of a lambda abstraction \\(\\lambda x.e\\) is of type \\(\\tau'\\) when \\(x\\) is of type \\(\\tau\\) then the whole lambda abstraction is of type \\(\\tau \\rightarrow \\tau'\\).
+{{< /latex >}}| __Abs__: If the body \\(e\\) of a lambda abstraction \\(\\lambda x.e\\) is of type \\(\\tau\'\\) when \\(x\\) is of type \\(\\tau\\) then the whole lambda abstraction is of type \\(\\tau \\rightarrow \\tau\'\\).
 {{< latex >}}
 \frac
     {\Gamma \vdash e : \tau \quad \text{matcht}(\tau, p_i) = b_i
@@ -81,7 +81,7 @@ Rule|Name and Description
 {{< latex >}}
 \frac{\Gamma \vdash e : \sigma \quad \sigma' \sqsubseteq \sigma}
     {\Gamma \vdash e : \sigma'}
-{{< /latex >}}| __Inst (New)__: If type \\(\\sigma'\\) is an instantiation of type \\(\\sigma\\) then an expression of type \\(\\sigma\\) is also an expression of type \\(\\sigma'\\).
+{{< /latex >}}| __Inst (New)__: If type \\(\\sigma\'\\) is an instantiation of type \\(\\sigma\\) then an expression of type \\(\\sigma\\) is also an expression of type \\(\\sigma\'\\).
 {{< latex >}}
 \frac
     {\Gamma \vdash e : \sigma \quad \alpha \not \in \text{free}(\Gamma)}
@@ -96,7 +96,20 @@ represents one (hence, "mono-"), concrete type. This is obvious in the case
 of \\(\\text{Int}\\) and \\(\\text{Int} \\rightarrow \\text{Bool}\\), but
 for \\(a \\rightarrow b\\) things are slightly less clear. Does it really
 represent a single type, if we can put an arbtirary thing for \\(a\\)?
-The answer is "no". The way it is right now, \\(a\\) is still an
-unknown, yet concrete thing. Once we find \\(a\\) and put it in,
-that's it. If only there was a way to say, "this is the type
-for any \\(a\\)"...
+The answer is "yes"! Although \\(a\\) is not currently known, it stands
+in place of another monotype, which is yet to be determined.
+
+So, how do we represent polymorphic types, like that of \\(\\text{if}\\)?
+We borrow some more notation from mathematics, and use the "forall" quantifier:
+
+{{< latex >}}
+\text{if} : \forall a \; . \; \text{Bool} \rightarrow a \rightarrow a \rightarrow a
+{{< /latex >}}
+
+This basically says, "the type of \\(\\text{if}\\) is \\(\\text{Bool} \\rightarrow a \\rightarrow a \\rightarrow a\\)
+for all possible \\(a\\)". This new expression using "forall" is what we call a type scheme, or a polytype \\(\\sigma\\).
+For simplicity, we only allow "forall" to be at the front of a polytype. That is, expressions like
+\\(a \\rightarrow \\forall b \\; . \\; b \\rightarrow b\\) are not valid polytypes as far as we're concerned.
+
+It's key to observe that the majority of the typing rules in the above table use monotypes (\\(\\tau\\)). Only
+two rules seem to mention \\(\\sigma\\): __Inst__ and __Gen__.