fix definition of WHom, close #597
mention Sigmas as subtypes in section 1.11
Explain equalities in Remark 1.12.1, close #516
unmarked errata for c4381c0
oops, use cleveref
fix notation for W-types
unmarked errata for bceb7ca
unmarked errata for f9e542b
Merge pull request #604 from mikeshulman/wtypes

fix notation for W-types, close #603
Merge pull request #605 from mikeshulman/whom

fix definition of WHom, close #597
Mark Errata (auto)
change some non-dependent Pis to arrows in chapter 5
reorder intro to emphasize compatibility with classical logic
Merge pull request #611 from mikeshulman/nondeppi

change some non-dependent Pis to arrows in chapter 5
double oops
Merge pull request #599 from mikeshulman/remark1.12.1

fix Remark 1.12.1, close #516
Mark Errata (auto)
"intuitionistic" means in the sense of Heyting
Merge pull request #616 from mikeshulman/classicality3

Clarify classical, constructive, intuitionistic in intro
fix typos in section 5.3, see #615