Manfred comments on Type Theory quick question

[Manfred]

The HoTT book is pretty readable, but I’m not in a position to evaluate its actual goodness.