?
Extra-Logical Proof-Theoretic Semantics in Homotopy Type Theory
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 it was generally
viewed as fundamentally mistaken or at least wholly outdated. However
the recently emerged Homotopy Type theory (HoTT) and the related program
of building new \univalent" foundations of mathematics provide a formal and
conceptual basis for revising, once again, the epistemic role and logical function
of extra-logical constructions in mathematical (and other) proofs [2].