Митчелл Райли, Линейная гомотопическая теория типов

Доклады на электронном семинаре по гомотопической теории типов, 20.01.2022 https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html Некоторые ∞-топозы поддерживают конструкции, которые по своей природе являются «линейными», такие как внешнее произведение параметризованных спектров. Их нельзя аксиоматически добавить к обычной гомотопической теории типов, поскольку нет способа обеспечить эту линейность: нет ограничений на использование переменных. В этом докладе описывается расширение гомотопической теории типов с линейными тензорами и гомотопическими формирователями типов, как своего рода «бинарная модальность» и её правый сопряженный. Стремление к совместимости с существующими результатами в гомотопической теории типов естественным образом приводит нас к новому типу сгруппированной зависимой теории типов. Наша теория типов призвана быть максимально удобной для человека, с прицелом на синтетическую стабильную гомотопическую теорию.