Алгебраическая топология
Если говорить о настоящей математике, из которой родилась современная формальная философия в виде модальной HoTT, как развитии идей Ловира, Категорного анализа, Алгебраической топологии, то мы сразу переходим к третьей полке моей библиотеки.
Для моделировании CW-комплексов понадобилось расширить стандарную типовую систему полиномиальных функторов до гомотопической реализации. Язык, где можно управлять гомотопическими кубами и CW-комплексами непосредственно, вместе с кванторами всеобщности и существования (локальной декартовой замкнутости) дает внутренний язык инфинити топоса. Поэтому логично, что истоки математики которая родила HoTT нужно искать в алгебраической топологии, которая изучает (ко)гомотопические и (ко)гомологические группы (ко)комплексов. В то время как гомотопические группы интернализируются в HoTT естественным образом, гомологии, и более того когомологии требуют значительной просадки по обширным алгебраическим сигнатурам.
Алгебраическая топология 515.14 и специальная алгебра 512.6
Теория гомотопий. Х.Сы-Цзян. 1964. УДК 515.143
Теория пучков. Г.Бредон. 1988. УДК 515.14
Универсальная алгебра. П.Кон. 1968. УДК 512.8
Введение в теорию категорий и функторов.
И.Бакур, А.Деляну. 1972. УДК 512.667
Категории частных и теория гомотопий. П.Габриель, М.Цисман. 1971. УДК 512
Алгебраическая топология и теория пучков. Р.Годеман. 1961. УДК 515.14
Симплектическая геометрия. А.Фоменко. 1988. УДК 515.14
Введение в гомологическую теорию размерности. П.Александров. 1975. УДК 512
Лекции по алгебраической топологии. А.Дольд. 1976. УДК 512.66
Гомология. С.Маклейн. 1966. УДК 512.66
Гомотопическая топология. Д.Фукс, А.Фоменко, В.Гутенмахер. 1969. УДК 515.143
Курс гомотопической топологии. А.Фоменко, Д.Фукс. 1989. УДК 515.143
Теория гомологий и когомологий. У.Масси. 1981. УДК 515.14
Алгебраическая топология. Введение У.Масси, Дж.Столлингс. 1977. УДК 515.14
Алгебраическая топология. Э.Спеньер. 1971. УДК 515.14
Основания алгебраической топологии. Н.Стиндрод, С.Эйленберг. 1958. УДК 515.14
Когомологические операции. .Стиндрод, Д.Эпстейн. 1983. УДК 515.143.5
Расслоенные пространства. Д.Хьюзмоллер. 1970. УДК 515.145.2
Современные проблемы математики. Топология-1. С.Новиков, Д.Фукс. 1986. УДК 515.14
Современные проблемы математики. Топология-2. О.Виро, Д.Фукс. 1988. УДК 515.14
Алгебраическая топология — гомотопии и гомологии. Р.Свитцер. 1985. УДК 515.14
Алгебраическая топология. А.Хатчер. 2011. УДК 512.515.14
Теория гомологий. Введение в алгебраическую топологию.
П.Хилтон, С.Уайли. 1965. УДК 512.66
Методы гомологической алгебры. Том 1. Введение в теорию когомологий и произведеные категории.
С.Гельфанд, Ю.Манин. 1988. УДК 512.66
Лекции по алегбраической топологии. Основы теории гомотопий.
М.Постников. 1984. УДК 515.14
Лекции по алегбраической топологии. Теория гомотопий клеточных пространств.
М.Постников. 1985. УДК 515.14
Elementary Applied Topology. R.Ghrist. 2014. УДК 512
Higher Topos Theory. J.Lurie. 2009. УДК 512
Local Homotopy Theory. J.Jardine. 2009. УДК 512
The Heart of Cohomology. G.Kato. 2006. УДК 512
Стабильные гомотопии и обобщенные гомологии. Дж.Адамс. 2013. УДК 515.14
В поисках формального рая для формализации на кубических тайпчекерах, теория категорий, абстрактная алгебра, теории (ко)гомологий не дают полного удовлетворения. Сигнатуры громоздкие, теория раздувается очень быстро, особенно в симплициальных моделях. Поэтому я нашел рай, или как инженеры говорят "правильное применение" которое гарантирует удовлетворение от использования по применению HoTT, которое возникает при моделировании дифференциальной геометрии. Все сигнатуры становятся компактными, тонны категорного кода редуцируется до естественного гомотопического кодирования инфинитизимальный дисков в кубической теории, правда работает это только в модальной версии HoTT.
Алгебраические конструкции 512.66
Как бонус абстрации новый раздел алгебраической топологии теория К-функторов. Когда раздутых категориальных сигнатур мало.
К-Теория. Введение. М.Каруби. 1981. УДК 512.667
Лекции по К-Теории. М.Атья. 1967. УДК 512.667
Алгебраическая К-Теория. Х.Басс. 1973. УДК 512.667