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