Univalence and Constructive Identity

АБВ
АБВ
АБВ

Обычная версия сайта

Приоритетные направления

по году

Тематика

6 ноября 2026 г.

Ученые НИУ ВШЭ - Санкт-Петербург разработали новый инструмент для речевой терапии после инсульта

Ученые НИУ ВШЭ — Санкт-Петербург совместно с коллегами из отделения нейрореабилитации Федерального Сибирского научно-клинического центра ФМБА в Красноярске разработали корпус упрощенных текстов для пациентов с афазией разной степени тяжести. Клинические исследования показали, что материалы по актуальным тематикам мотивируют активнее заниматься восстановлением речи после инсульта. Исследование опубликовано в журнале Aphasiology.

3 ноября 2026 г.

Физики научили ИИ настраивать пучок частиц в ускорителе

Исследователи Института искусственного интеллекта и цифровых наук ФКН НИУ ВШЭ и Института ядерной физики СО РАН разработали RLABC — программу, которая помогает подбирать оптимальные настройки ускорителя частиц с помощью обучения с подкреплением. В компьютерном эксперименте программа настроила модель так, что до конца ускорителя доходило около 70% частиц. Исследование опубликовано в журнале Computer Physics Communications.

3 ноября 2026 г.

«Органы на чипе позволяют проверять лекарства без экспериментов на животных»

Лаборатория молекулярной физиологии факультета биологии и биотехнологии НИУ ВШЭ изучает, как молекулярные регуляторы (микроРНК) управляют работой генов и влияют на развитие болезней — онкологических, вирусных и воспалительных, а также осложнений беременности. В Вышке выращивают модели органов человека на чипе: крошечные устройства с живыми клетками, воспроизводящие работу, например, плаценты или кишечника. Модели помогают понять, как возникают болезни и как на них действуют лекарства. «Вышка.Главное» побеседовала с заведующим лабораторией Евгением Князевым.

Нашли опечатку?
Выделите её, нажмите Ctrl+Enter и отправьте нам уведомление. Спасибо за участие!

Публикации

?

Univalence and Constructive Identity

P. 170–174.

Родин А. В.

The non-standard identity concept developed in the Homotopy Type theory allows for an alternative analysis of
Frege’s famous Venus example, which explains how empirical evidences justify judgements about identities and accounts for
the constructive aspect of such judgements.

Язык: английский

В книге

Philosophy, Mathematics, Linguistics: Aspects of Interaction (PhML 2012)

St. Petersburg: ВВМ, 2012.

Models of HoTT and the Constructive View of Theories

Родин А. В., , in: Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts.: Springer, 2019. Ch. 9 P. 191–219.

Добавлено: 30 октября 2019 г.

Extra-Logical Proof-Theoretic Semantics in Homotopy Type Theory

Родин А. В., , in: Одиннадцатые Смирновские чтения по логике: материалы Международной научной конференции, 19 – 21 июня 2019, г. Москва.: М.: Современные тетради, 2019. P. 42–43.

Добавлено: 30 июня 2019 г.

Model structures on categories of models of type theories

Valery Isaev, Mathematical Structures in Computer Science 2018 Vol. 28 No. 10 P. 1695–1722

Добавлено: 6 ноября 2018 г.

Constructive Identities for Physics

Родин А. В., , in: Frontiers of Fundamental Physics 14Vol. 224: EPISTEMOLOGY AND PHILOSOPHY.: [б.и.], 2014.

Homotopy Type theory instantiates a new form of axiomatic approach, which is more friendly to physics than the standard axiomatic approach stemming from Hilbert. This new axiomatic approach combines logical and geometrical methods in a new way and brings about a non-trivial constructive concept of identity applicable in various physical contexts including Quantum Mechanics and General Relativity. ...

Добавлено: 6 июня 2018 г.

Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts.

Springer, 2019.

Homotopy Type theory and its Model theory provide a novel formal semantic framework for representing scientic theories. This framework supports a constructive view of theories according to which a theory is essentially characterised by its methods. The constructive view of theories was earlier defended by Ernest Nagel and a number of other philosophers of the past but available logical ...

Добавлено: 5 июня 2018 г.

Venus Homotopically

Родин А. В., IfCoLoG Journal of Logics and their Applications 2017 Vol. 4 No. 4 P. 1427–1446

The identity concept developed in the Homotopy Type theory (HoTT) supports an analysis of Frege's famous Venus example, which explains how empirical evidences justify judgements about identities. In the context of this analysis we consider the traditional distinction between the extension and the intension of concepts as it appears in HoTT, discuss an ontological signicance ...

Добавлено: 5 июня 2018 г.

On the Constructive Axiomatic Method

Родин А. В., Logique et Analyse 2018 Vol. 242 No. 2 P. 201–231

Добавлено: 26 мая 2018 г.