Univalence and Constructive Identity

АБВ
АБВ
АБВ

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

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

по году

Тематика

1 сентября 2026 г.

Ученые НИУ ВШЭ создали новый корпус детской русской речи

Исследователи Центра языка и мозга НИУ ВШЭ представили RusLan-M — открытый мультимедийный корпус, который позволяет проследить развитие русской речи у детей от первых слов до появления сложных грамматических конструкций. В базе собраны около 41 часа видеозаписей и более 35 тысяч детских высказываний. Новый ресурс поможет ученым точнее изучать, как дети осваивают русский язык, а в перспективе — создавать более надежные инструменты для оценки речевого развития. Исследование опубликовано в журнале Language Resources and Evaluation.

31 августа 2026 г.

Ученые НИУ ВШЭ предложили по-новому считать неформальную занятость в России

Действующие подходы Росстата к оценке неформальной занятости в России уже не в полной мере отражают современную ситуацию на рынке труда. К такому выводу в своем исследовании пришли экономисты ИСИЭЗ НИУ ВШЭ. Ученые считают, что новые международные стандарты помогут получать более достоверные данные о рынке труда, а значит, принимать более эффективные государственные решения.

28 августа 2026 г.

МИЭМ ВШЭ и МИЭТ договорились о научном сотрудничестве

26 августа Московский институт электроники и математики им. А.Н. Тихонова (МИЭМ) ВШЭ и Национальный исследовательский университет «Московский институт электронной техники» (МИЭТ) подписали договор о сотрудничестве. Соглашение направлено на развитие совместных исследований в области физики, перспективного материаловедения и электроники, объединяющих экспериментальные и вычислительные подходы, выполнение совместных опытно-конструкторских работ, а также подготовку заявок на российские и международные научные гранты.

Нашли опечатку?
Выделите её, нажмите 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 г.