diff --git a/src/subtyping.md b/src/subtyping.md
index 41cf17a..f0caf71 100644
--- a/src/subtyping.md
+++ b/src/subtyping.md
@@ -3,15 +3,15 @@
 Subtyping is a relationship between types that allows statically typed
 languages to be a bit more flexible and permissive.
 
-Subtyping in Rust is a bit different from subtyping in other languages. This leads
-to examples of subtyping being *a bit* convoluted. This is especially unforunate
-because subtyping, and especially variance, are actually really hard to
-understand properly. As in, even compiler writers mess it up all the time.
+Subtyping in Rust is a bit different from subtyping in other languages. This
+makes it harder to give simple examples, which is a problem since subtyping,
+and especially variance, are already hard to understand properly. As in,
+even compiler writers mess it up all the time.
 
-In order to make examples that are simple and concise, this section will consider a
-*small* extension to the Rust language to introduce subtyping in a way that is more
-similar to other languages. After establishing concepts and issues under this simpler
-system, we will then relate it back to how subtyping actually occurs in Rust.
+To keep things simple, this section will consider a small extension to the
+Rust language that adds a new and simpler subtyping relationship. After
+establishing concepts and issues under this simpler system,
+we will then relate it back to how subtyping actually occurs in Rust.
 
 So here's our simple extension, *Objective Rust*, featuring three new types:
 
@@ -51,17 +51,17 @@ love(mr_snuggles);         // ERROR: expected Animal, found Cat
 
 Mr. Snuggles is a Cat, and Cats aren't *exactly* Animals, so we can't love him! 😿
 
-This is especially annoying because Cats *are* Animals. They support every operation
+This is annoying because Cats *are* Animals. They support every operation
 an Animal supports, so intuitively `love` shouldn't care if we pass it a `Cat`.
-Or, to put it another way, we should be able to just *forget* the non-animal
-parts of our `Cat`, as they aren't necessary to love it.
+We should be able to just **forget** the non-animal parts of our `Cat`, as they
+aren't necessary to love it.
 
 This is exactly the problem that *subtyping* is intended to fix. Because Cats are just
-Animals *and more*, we say Cat is a *subtype* of Animal (because Cats are a *subset*
-of all the Animals). Equivalently, we can say that Animal is a *supertype* of Cat.
+Animals **and more**, we say Cat is a *subtype* of Animal (because Cats are a *subset*
+of all the Animals). Equivalently, we say that Animal is a *supertype* of Cat.
 With subtypes, we can tweak our overly strict static type system
-with a simple rule: anywhere a value of some type `T` is expected, we *also* accept
-values that are *subtypes* of `T`.
+with a simple rule: anywhere a value of type `T` is expected, we will also
+accept values that are subtypes of `T`.
 
 Or more concretely: anywhere an Animal is expected, a Cat or Dog will also work.
 
@@ -72,7 +72,7 @@ write unsafe code, the compiler will automatically handle all the corner cases f
 But this is the Rustonomicon. We're writing unsafe code, so we need to understand how
 this stuff really works, and how we can mess it up.
 
-The core problem is that this rule, naively applied, will lead to *Meowing Dogs*. That is,
+The core problem is that this rule, naively applied, will lead to *meowing Dogs*. That is,
 we can convince someone that a Dog is actually a Cat. This completely destroys the fabric
 of our static type system, making it worse than useless (and leading to Undefined Behaviour).
 
@@ -96,7 +96,8 @@ fn main() {
 ```
 
 Clearly, we need a more robust system than "find and replace". That system is *variance*,
-the rules governing how subtyping *composes*.
+which is a set of rules governing how subtyping should compose. Most importantly, variance
+defines situations where subtyping should be disabled.
 
 But before we get into variance, let's take a quick peek at where subtyping actually occurs in
 Rust: *lifetimes*!
@@ -116,7 +117,8 @@ just as `'big` is `'small` *and more*.
 Put another way, if someone wants a reference that lives for `'small`,
 usually what they actually mean is that they want a reference that lives
 for *at least* `'small`. They don't actually care if the lifetimes match
-exactly. So it should be ok for us to *forget* that we live for `'big`.
+exactly. So it should be ok for us to **forget** that something lives for
+`'big` and only remember that it lives for `'small`.
 
 The meowing dog problem for lifetimes will result in us being able to
 store a short-lived reference in a place that expects a longer-lived one,
@@ -124,12 +126,12 @@ creating a dangling reference and letting us use-after-free.
 
 It will be useful to note that `'static`, the forever lifetime, is a subtype of
 every lifetime because by definition it outlives everything. We will be using
-this relationship frequently in examples.
+this relationship in later examples to keep them as simple as possible.
 
 With all that said, we still have no idea how to actually *use* subtyping of lifetimes,
 because nothing ever has type `'a`. Lifetimes only occur as part of some larger type
 like `&'a u32` or `IterMut<'a, u32>`. To apply lifetime subtyping, we need to know
-how to *compose* subtyping. Once again, we need *variance*.
+how to compose subtyping. Once again, we need *variance*.
 
 
 
@@ -140,8 +142,8 @@ Variance is where things get a bit complicated.
 
 Variance is a property that *type constructors* have with respect to their
 arguments. A type constructor in Rust is any generic type with unbound arguments.
-For instance `Vec` is a type constructor that takes a type `X` and returns
-`Vec<X>`. `&` and `&mut` are type constructors that take two inputs: a
+For instance `Vec` is a type constructor that takes a type `T` and returns
+`Vec<T>`. `&` and `&mut` are type constructors that take two inputs: a
 lifetime, and a type to point to.
 
 > NOTE: For convenience we will often refer to `F<T>` as a type constructor just so
@@ -158,7 +160,7 @@ types `Sub` and `Super`, where `Sub` is a subtype of `Super`:
 If `F` has multiple type parameters, we can talk about the individual variances
 by saying that, for example, `F<T, U>` is covariant over `T` and invariant over `U`.
 
-It is *very useful* to keep in mind that covariance is, in practical terms, "the"
+It is very useful to keep in mind that covariance is, in practical terms, "the"
 variance. Almost all consideration of variance is in terms of whether something
 should be covariant or invariant. Actually witnessing contravariance is quite difficult
 in Rust, though it does in fact exist.
@@ -178,7 +180,7 @@ to trying to explain:
 |   | *const T      |           | covariant         |           |
 |   | *mut T        |           | invariant         |           |
 
-These types with \*'s are the ones we will be focusing on, as they are in
+The types with \*'s are the ones we will be focusing on, as they are in
 some sense "fundamental". All the others can be understood by analogy to the others:
 
 * Vec and all other owning pointers and collections follow the same logic as Box
@@ -190,9 +192,9 @@ some sense "fundamental". All the others can be understood by analogy to the oth
 > a function, which is why it really doesn't come up much in practice. Invoking
 > contravariance involves higher-order programming with function pointers that
 > take references with specific lifetimes (as opposed to the usual "any lifetime",
-> which gets into higher rank lifetimes which work independently of subtyping).
+> which gets into higher rank lifetimes, which work independently of subtyping).
 
-Ok, that's enough type theory! Let's try to apply the concept of variance to Rust,
+Ok, that's enough type theory! Let's try to apply the concept of variance to Rust
 and look at some examples.
 
 First off, let's revisit the meowing dog example:
@@ -229,28 +231,29 @@ to modify the original value *when we don't remember all of its constraints*.
 And so, we can make someone have a Dog when they're certain they still have a Cat.
 
 With that established, we can easily see why `&T` being covariant over `T` *is*
-sound: it doesn't let you modify the value, only look at it. Without anyway to
+sound: it doesn't let you modify the value, only look at it. Without any way to
 mutate, there's no way for us to mess with any details. We can also see why
-UnsafeCell and all the other interior mutability types must be invariant: they
+`UnsafeCell` and all the other interior mutability types must be invariant: they
 make `&T` work like `&mut T`!
 
 Now what about the lifetime on references? Why is it ok for both kinds of references
-to be covariant over their lifetimes. Well, here's a two-pronged argument:
+to be covariant over their lifetimes? Well, here's a two-pronged argument:
 
 First and foremost, subtyping references based on their lifetimes is *the entire point
 of subtyping in Rust*. The only reason we have subtyping is so we can pass
 long-lived things where short-lived things are expected. So it better work!
 
-Second, and more seriously, references *own* their lifetimes, while they are
-only borrowing their referents. If you shrink down a reference's lifetime when
-you hand it to someone, that location now has a reference which owns the smaller
-lifetime. There's no way to mess with original reference's lifetime using the
-other one.
+Second, and more seriously, lifetimes are only a part of the reference itself. The
+type of the referent is shared knowledge, which is why adjusting that type in only
+one place (the reference) can lead to issues. But if you shrink down a reference's
+lifetime when you hand it to someone, that lifetime information isn't shared in
+anyway. There are now two independent references with independent lifetimes.
+There's no way to mess with original reference's lifetime using the other one.
 
-Or rather, the only way to mess with someone's lifetime is to build a meowing dog,
-and as soon as you try to build a meowing dog the lifetime should be wrapped up
-in an invariant context, preventing the lifetime from being shrunk. That's probably
-a little too abstract, so let's port the meowing dog problem over to real Rust.
+Or rather, the only way to mess with someone's lifetime is to build a meowing dog.
+But as soon as you try to build a meowing dog, the lifetime should be wrapped up
+in an invariant type, preventing the lifetime from being shrunk. To understand this
+better, let's port the meowing dog problem over to real Rust.
 
 In the meowing dog problem we take a subtype (Cat), convert it into a supertype
 (Animal), and then use that fact to overwrite the subtype with a value that satisfies
@@ -293,7 +296,7 @@ error[E0597]: `spike` does not live long enough
    = note: borrowed value must be valid for the static lifetime...
 ```
 
-Good! It doesn't compile! Let's break down what's happening here in detail.
+Good, it doesn't compile! Let's break down what's happening here in detail.
 
 First let's look at the new `evil_feeder` function:
 
@@ -312,12 +315,12 @@ Meanwhile, in the caller we pass in `&mut &'static str` and `&'spike_str str`.
 Because `&mut T` is invariant over `T`, the compiler concludes it can't apply any subtyping
 to the first argument, and so `T` must be exactly `&'static str`.
 
-`&'a str` *is* covariant over `'a` so the compiler adopts a constraint: `&'spike_str str`
-must be a subtype of `&'static str` (inclusive), which in turn implies `'spike_str`
-must be subtype `'static` (inclusive). Which is to say, `'spike_str` must contain
-`'static`. But only one thing contains `'static` -- `'static` itself!
+The other argument is only an `&'a str`, which *is* covariant over `'a`. So the compiler
+adopts a constraint: `&'spike_str str` must be a subtype of `&'static str` (inclusive),
+which in turn implies `'spike_str` must be a subtype of `'static` (inclusive). Which is to say,
+`'spike_str` must contain `'static`. But only one thing contains `'static` -- `'static` itself!
 
-This is why we get the error when we try to assign `&spike` to `spike_str`. The
+This is why we get an error when we try to assign `&spike` to `spike_str`. The
 compiler has worked backwards to conclude `spike_str` must live forever, and `&spike`
 simply can't live that long.
 
@@ -326,12 +329,12 @@ whenever they're put into a context that could do something bad with that. In th
 we inherited invariance as soon as we put our reference inside an `&mut T`.
 
 As it turns out, the argument for why it's ok for Box (and Vec, Hashmap, etc.) to
-be covariant is pretty similar to the argument for why it's ok for why it's ok for
+be covariant is pretty similar to the argument for why it's ok for
 lifetimes to be covariant: as soon as you try to stuff them in something like a
 mutable reference, they inherit invariance and you're prevented from doing anything
-bad!
+bad.
 
-However Box makes it easier to focus on the *owning* aspect of references that we
+However Box makes it easier to focus on by-value aspect of references that we
 partially glossed over.
 
 Unlike a lot of languages which allow values to be freely aliased at all times,
@@ -351,8 +354,8 @@ pet = spike;
 
 There is no problem at all with the fact that we have forgotten that `mr_snuggles` was a Cat,
 or that we overwrote him with a Dog, because as soon as we moved mr_snuggles to a variable
-that only knew he was an Animal, *we destroyed the only thing in the universe that
-rememembered he was a Cat*!
+that only knew he was an Animal, **we destroyed the only thing in the universe that
+remembered he was a Cat**!
 
 In contrast to the argument about immutable references being soundly covariant because they
 don't let you change anything, owned values can be covariant because they make you
@@ -361,8 +364,9 @@ Applying by-value subtyping is an irreversible act of knowledge destruction, and
 without any memory of how things used to be, no one can be tricked into acting on
 that old information!
 
-Only one thing left to explain: function pointers. To see why
-`fn(T) -> U` should be covariant over `U`, consider the following signature:
+Only one thing left to explain: function pointers.
+
+To see why `fn(T) -> U` should be covariant over `U`, consider the following signature:
 
 ```rust,ignore
 fn get_animal() -> Animal;
@@ -407,7 +411,9 @@ Now, this is all well and good for the types the standard library provides, but
 how is variance determined for type that *you* define? A struct, informally
 speaking, inherits the variance of its fields. If a struct `MyType`
 has a generic argument `A` that is used in a field `a`, then MyType's variance
-over `A` is exactly `a`'s variance. However if `A` is used in multiple fields:
+over `A` is exactly `a`'s variance over `A`.
+
+However if `A` is used in multiple fields:
 
 * If all uses of `A` are covariant, then MyType is covariant over `A`
 * If all uses of `A` are contravariant, then MyType is contravariant over `A`