fix notation
use subsections instead of paragraphs in HoTT section
give proof sketch for set-ness of inductive types like N
insert reference
improve discussion of \PT vs \BT