Cette question posée par un physicien porte sur la correspondance entre les deux plans : Idée mathématique et monde
« From all the logics lingua which HoTT provides from the start, what of it becomes something physical/something in the world?«
Réponse rapide :
« The quick answer to the question is the following somewhat remarkable statement
Identity types in the new foundations of mathematics in homotopy type theory correspond in physics to spaces of gauge transformations and higher order gauge transformations.
Notably when the homotopy type theory is equipped with the additional axtiom of differential cohesion, then one can “differentiate” identity types. Their infinitesimal version are the BRST complexes famous from gauge theory. Or rather: a “ghost” in a BRST complex is a tangent to a term in an identity type, a ghost-of-ghosts is a tangent to a term in an identity-type-of-an-identity-type and so forth.«
« So when you are asking how identity types reflect to “something in the world” you just need to look for cases where gauge transformations have a worldly incarnation. Examples of course are abound. Consider the theory of instantons and remember that standard QCD theory says that the vacuum which we inhabit is an instanton sea with about one instanton per femtometer. This means that the physical reality which we inhabit, if you remove everything and just consider the plain vacuum, is already densely filled with, if you wish, physical incarnation of identity types.
Generally, this is what the foundation of physics in higher geometry/higher topos theory/homotopy type theory is all about: to correctly take into account not just perturbative effects, but to take into account the full non-perturbative structure of gauge theory, all the “large” gauge transformations, all the quantum anomalies, all the global effects. Geometric homotopy theory (higher moduli stacks) is the mathematical language to do so, and the pleasing insight of Vladimir Voevodsky and others is that this in turn happens to have a profund syntactic/logic formulation in homotopy type theory.«
Des liens sont indiqués :