setmath: remove underscores in labels
homotopy: fix a reference in van Kampen
basics: mention impredicativity of hprop
basics: defining brck in terms of impredicativity