mention Sigmas as subtypes in section 1.11
Explain equalities in Remark 1.12.1, close #516
unmarked errata for c4381c0
oops, use cleveref
reorder intro to emphasize compatibility with classical logic
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
clarify intensional/extensional in ch 2 notes, close #600
fix typos in section 5.3, see #615
unmarked errata for 7c54e9f
Merge branch 'master' into wtypes

Conflicts:
	errata.tex
Merge pull request #618 from mikeshulman/wtypes

fix typos in section 5.3, see #615
Mark Errata (auto)
fixed identity eliminator typos in appendix: ind' replaced with ind
appended errata
added label for identity type subsection
fixed previous errata commit