Egbert Rijke - Introduction to Homotopy Type Theory (Dec 2022)

Активное влияние на написание книги оказывали: Steve Awodey, Dan Grayson, Andrej Bauer

Ранние версии книги читали и обсуждали: William Barnett, Katja Berčič, Marc Bezem, Ulrik Buchholtz, Ali Caglayan, Dan Christensen, Thierry Coquand, Peter Dybjer, Jacob Ender, Martín Escardó, Sam van Gool, Kerem Güneş, Bob Harper, Matej Jazbec, Urban Jezernik, Tom de Jong, Ivan Kobe, Anders Mortberg, Clive Newstead, Charles Rezk, Emily Riehl, Mike Shulman, Elif Uskuplu, Chetan Vuppulury, Blaž Zupančič

Начал читать -- по-моему, выглядит потрясающим введением, намного более функциональным для начинающего, чем HoTT Book. Не предполагает пререквизитов в теории типов.
(UPD 14.10.2023 После понимания основ по этой книге, рекомендую переключаться на существенно более богатую темами HoTT Book)

Очень хочется, по возможности, везде уже переходить на этот язык -- многое будет становится более естественно и ясно (вчера вот перечитал, например: anafunctor; вспоминается также this). Если действительно (как я надеюсь) несложно быстро переводить любого через языковой барьер при необходимости. На самом деле, у меня сложилось впечатление, что вот такое изучение языка в реальных курсах, как правило, получается намного более интересным и эффективным, чем изучение его самого по себе (хотя и одна лекция под введение, конечно, необходима).