Доклад Арнольда Григоряна «Унивалентные основания и конструктивная теория типов»
4 октября в 18:30 состоится заседание научно-исследовательского семинара «From the Logical Point of View».
Арнольд Григорян
НИУ ВШЭ
выступит с докладом на тему
«Унивалентные основания и конструктивная теория типов»
Аннотация.
Программа унивалентных оснований была инициирована Владимиром Воеводским для разработки новой теории типов, удобной для формализации математики. Результатом, среди прочего, стало появление гомотопической интерпретации теории типов Мартина-Лёфа, которой будет посвящен доклад. Первая часть будет посвящена введению в теорию типов и ее констуктивной интерпретации. После этого я представлю аксиому унивалентности и покажу ее связь с типом тождества. В конце доклада планируется обсуждение проблем унивалентной теории типов, а также логического и философского значения аксиомы унивалентности.