Дэн Кристенсен: «Рассуждения в ∞-топосе с использованием теории гомотопических типов»

1 апреля 2021 г. Часть коллоквиума Института Топосов. - Аннотация: Этот доклад станет введением в гомотопическую теорию типов и объяснит, как её можно использовать для доказательства теорем, справедливых в любом ∞-топосе. Я представлю основные идеи теории типов и дам некоторое интуитивное понимание того, что они означают в гомотопическом контексте. В заключение я приведу примеры результатов, доказанных в гомотопической теории типов, которые сообщают нам новые результаты в любом ∞-топосе. Предварительные знания теории типов или теории ∞-категорий не предполагаются.