Consider clarification in section 5.1

[TomasPuverle]

In the The Identity Monad section, it says

failed to synthesize instance
  HAdd Nat Nat (?m.9063 ?m.9065)

"In this error, the application of one metavariable to another indicates that Lean doesn't run the type-level computation backwards."

I think the intent is to imply that one cannot go from Nat via the inverse of the Id function to obtain Id Nat; and that the metavariables stand for the m type application (I think). However, since that was the first mention of "the type-level computation", perhaps the wording could be clarified a little?

[david-christiansen]

Thank you, this is very useful feedback!