7
$\begingroup$

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?

Improve this question
$\endgroup$
8
  • $\begingroup$ @Trimok: I've added a link. It (the type, as in programming) is the proposition of equality of two things. From a computational standpoint, it's the collection of justifications for this proposition. In HoTT it's also geometric - it's a path space "$I\to \mathcal M$". I tried to understnad identity types as sub"sets" of hom-sets in a question on the Math board and this answer might be helpful. If you read this, let's delete this list of comments here. $\endgroup$
    – Nikolaj-K
    Commented Dec 10, 2013 at 22:05
  • $\begingroup$ Don' t you have any information in the chapter $5$ (Applications) (from page $577$) of the Urs Schreiber 's arxiv paper ? $\endgroup$
    – Trimok
    Commented Dec 11, 2013 at 10:39
  • $\begingroup$ @Trimok: I lose track of the identies around p.200 when he introduces types but emphasises the connection to the more categorical language. Physics seems to pop up at p.387. What I would have expected going into it is that fields are terms of a product type and the identity types over these are the gauge equivalences. On page p.397 he has a table with equivalences between physically "reasonable" things and notions of (cohesive) HoTT, but there I only see equivalences (they might just be identites by univalence, or so). But truth is I don't even quite know what to think when I see a $\bf{B}$. $\endgroup$
    – Nikolaj-K
    Commented Dec 11, 2013 at 12:55
  • 1
    $\begingroup$ Maybe you will have more answers by changing your tags, and put, quantum-field-theory, research-level, mathematical-physics $\endgroup$
    – Trimok
    Commented Dec 13, 2013 at 10:12
  • 1
    $\begingroup$ Although I haven't made it far enough into Urs' paper to answer (nor am I likely to have much time to go further in the coming months), you might want to head over to the n-category cafe post by David Corfield about Urs' paper and point them towards your question. There are likely a few people in the comment section there who can help you out. $\endgroup$
    – Ralph Mellish
    Commented Jan 22, 2014 at 13:57

1 Answer 1

Reset to default
7
$\begingroup$

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

Improve this answer
$\endgroup$
5
  • $\begingroup$ Thanks for the answer, I'm working to understand it. I imagine you'd like to see my follow-up question, which is more concrete. $\endgroup$
    – Nikolaj-K
    Commented Mar 23, 2014 at 14:44
  • $\begingroup$ Why do we need types "$=$" to begin with? After all, weak category theory can do without. Can you point me to why, in HoTT, we start out with an identity type and then impose $(A=B)\simeq(A\simeq B)$? Say we start out with a dependently typed theory (with $\prod, \sum$ in particular) and then define "$\simeq$" as is done in the HoTT book. If the principle of equivalence${}^{TM}$ is to be implemented with this axiom, why do we consider a theory with identity in the first place. It appears all we really want is "just" equivalence anyway. Btw. I lurk the nForum - is there a question section? $\endgroup$
    – Nikolaj-K
    Commented Nov 4, 2014 at 12:53
  • $\begingroup$ Or let me say: I get the need for path spaces, but do we need "equality proper" before we define equivalence and by this obtain the desired notion of equality? $\endgroup$
    – Nikolaj-K
    Commented Nov 4, 2014 at 13:08
  • $\begingroup$ Yes, the definition of "≃" involves "=". A function is an equivalence iff all its homotopy fibers are contractible, and in order to say "homotopy fiber" and "is contractible" one uses "=". In the models this is understood as: "=" sees the morphisms inside an object of an infinity-category, but "≃" sees the morphisms of the infinity-category itself. Now there is the objcect classifier which is a small image of the whole category inside itself. So in that particular object both kinds of morphisms are reflected and the univalence axiom says that they agree. So internal and external agree. $\endgroup$
    – Urs Schreiber
    Commented Nov 4, 2014 at 17:11
  • $\begingroup$ You are welcome to ask questions on the nForum. Just hit "Start a discussion" in the top left, select an appropriate discussion category, usually "Atrium: Mathematics, Physics and Philosophy", and go ahead. $\endgroup$
    – Urs Schreiber
    Commented Nov 4, 2014 at 17:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.