Rodin A., , in: Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts.: Springer, 2019. Ch. 9 P. 191–219.
Homotopy Type theory and its Model theory provide a novel formal
semantic framework for representing scientific 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 means ...
Added: October 30, 2019
Rodin A., , in: Одиннадцатые Смирновские чтения по логике: материалы Международной научной конференции, 19 – 21 июня 2019, г. Москва.: М.: Современные тетради, 2019. P. 42–43.
Kant famously argued that elementary geometrical statements such as
Euclid's Triangle Angle Sum theorem cannot be deduced from the rst principles
by purely logical means because their proofs require extra-logical geometrical
constructions [1, A719/B747]. The discovery of non-Euclidean geometries
in the 19-th century made Kant's analysis of geometrical reasoning untenable
in its original form, and throughout the following 20-th century ...
Added: June 30, 2019
Valery Isaev, Mathematical Structures in Computer Science 2018 Vol. 28 No. 10 P. 1695–1722
Models of dependent type theories are contextual categories with some additional structure. We prove that if a theory T has enough structure, then the category T-Mod of its models carries the structure of a model category. We also show that if T has Σ-types, then weak equivalences can be characterized in terms of homotopy categories ...
Added: November 6, 2018
Rodin A., , in: Philosophy, Mathematics, Linguistics: Aspects of Interaction (PhML 2012).: St. Petersburg: ВВМ, 2012. 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. ...
Added: June 6, 2018
Springer, 2019.
Homotopy Type theory and its Model theory provide a novel formal semantic
framework for representing scienti c 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 ...
Added: June 5, 2018
Rodin A., 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 signi cance ...
Added: June 5, 2018
Rodin A., Logique et Analyse 2018 Vol. 242 No. 2 P. 201–231
The received notion of axiomatic method stemming from Hilbert is not fully adequate to the recent successful practice of axiomatizing mathematical theories. The axiomatic architecture of Homotopy type theory (HoTT) does not ft the pattern of formal axiomatic theory in the standard sense of the word. However this theory falls under a more general and ...
Added: May 26, 2018