fix typos in section 6.9, close #554
errata for 2fc7fde
use arrow for non-dep. arg. of path ind. hypothesis in ch. 2, close #441
explain some acronyms, close #404
exercise on type equivalence as a congruence, close #493
Merge pull request #557 from mikeshulman/acronyms

explain some acronyms, close #404
Merge pull request #556 from mikeshulman/pinotation

use arrow for non-dep. arg. of path ind. hypothesis in ch. 2, close #441
Merge pull request #555 from mikeshulman/truncationtypos

fix typos in section 6.9, close #554
Merge pull request #558 from mikeshulman/tyeqcong

exercise on type equivalence as a congruence, close #493
Mark Errata (auto)