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
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 re 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:
