Are identity types interpreted physically in an infinity-topos formulation of equations of motion? In reference to Urs Schreibers paper/book on foundations of field theory Differential cohomology in a cohesive infinity-topos I wonder: are identity types there used "only" for the computations, or are they themselves at some point interpreted to represent some physical quantity? Can I think of the "path spaces" as something more concrete here? 
(edit: reference request in the comments: identity type in the nLab.)
They are what is implemented natively in the logic and I wonder if, then in the geometric framework, these become tied to some more concrete intuitive notions. And I mean on a level beyond the fact that that homotopies are arguably already visual and hence physical. I mean it similarly to how saying the Hamiltonian is the energy function gives more physicists insight than just stating it's a function on phase space, generating paths. 
So put differently: From all the logics lingua which HoTT provides from the start, what of it becomes something physical/something in the world?
 A: Here is a belated reply. (I come across this question only now, by chance. This was posted right when our daughter was born, which was kind of distracting for me...)
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.
One might put it this way: homotopy type theory is a new foundations of mathematics that has the gauge principle built right into it. The gauge principle in the sense that: it is wrong to ever ask if two field configurations are equal, we have to ask if there is a gauge equivalence relating them. And if there is more than one such, then it is wrong two ask if two gauge transformations are equal, instead we have to ask if there is a gauge-of-gauge transformation between them, and so ever on.
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.
Notice that nobody asked for this, this is a gift given to us by nature: you would have suspected that when we dig ever deeper into the mathematical structure of modern local gauge quantum field theory, that then it gets ever more complicated, ever more sophisticated: moduli stacks, differential cohomology, anomalies, etc. But in the light of homotopy type theory one finds that strikingly as one goes really to the bottom of it, then suddently at the foundations of gauge quantum field theory suddently things become conceptually simpler, in the sense of "simple beauty" in laws of physics. For instance in cohesive homotopy type theory there is an elegant way to directly speak of the twisted differential K-theory that is at the heart of Freed-Witten anomaly cancellation in 2d QFT. It's just there flowing in a few steps from the foundational axioms, instead of being the long convoluted construction as which it has appeared in research articles (here I am referring to stuff related to section 4.1.2).
I could go on, but maybe I should stop here. If my book seems to long, try the following two texts which are meant to quickly show the way from the bare foundations of cohesive homotopy type theory to local Lagrangian gauge field theory:


*

*Urs Schreiber and Michael Shulman, Quantum gauge field theory in Cohesive homotopy type theory, Proceedings of Quantum Physics and Logic (2012)

*Urs Schreiber, Homotopy-type semantics for quantization, at Modern Trends in Topological Quantum Field Theory (2014)
