Would like to be pointed at reactions to the Adv.Inst.Princeton HoTT book which can be appreciated by the relative layman, especially reactions which put it in the context of Human, Automated and Assisted Theorem Proving. Thanks in advance, Guy