Catching up with HoTT/HoTT

I was ca. 500 commits behind, but now most things are compliant with
the most recent HoTT branch.