Начал вчера читать The HOTT Book и после осиленной первой главы и просмотра различных обсуждений и гитхаба возникли подозрения.

Все-таки эта штука пишется и писалась коллективно. Похоже это больше полгигон/большой черовик и как учебник который поможет сформировать представление об областе, очень тяжко идет (лично у меня) Где-то текст ну чрезмерно запутан.

Попробую почитать Egbert Rijke, а еще нашел такую книженцию интересную "The little Typer"

#HOTT #math #typetheory