Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

September 13, 2016

HoTT and Philosophy

Posted by David Corfield

I’m down in Bristol at a conference – HoTT and Philosophy. Slides for my talk – The modality of physical law in modal homotopy type theory – are here.

Perhaps ‘The modality of differential equations’ would have been more accurate as I’m looking to work through an analogy in modal type theory between necessity and the jet comonad, partial differential equations being the latter’s coalgebras.

The talk should provide some intuition for a pair of talks the following day:

  • Urs Schreiber & Felix Wellen: ‘Formalizing higher Cartan geometry in modal HoTT’
  • Felix Wellen: ‘Synthetic differential geometry in homotopy type theory via a modal operator’

I met up with Urs and Felix yesterday evening. Felix is coding up in Agda geometric constructions, such as frame bundles, using the modalities of differential cohesion.

Posted at September 13, 2016 7:49 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2906



11 Comments & 0 Trackbacks

Re: HoTT and Philosophy

I like your slides. What is the attendance like? Urs’s and Felix’s titles sound very mathematical, but “HoTT and Philosophy” sounds like there would be a lot of philosophers there.

Posted by: Mike Shulman on September 14, 2016 4:02 AM | Permalink | Reply to this

Re: HoTT and Philosophy

Thanks, Mike.

It’s not a large conference, perhaps 20 or so attending. The majority are philosophers, some locals from Bristol dropping by, without HoTT being a central interest.

Urs’s slides are available. So, yes, very mathematical or mathematical physics-ish. It’s not so uncommon for philosophy of physics talks to be mathematically technical.

By the way, Felix has a repository for his code. He says there that he’s proved:

  • The formal disc bundle over a group is trivial.
  • The formal disc bundle over a GG-manifold is locally trivial.
Posted by: David Corfield on September 14, 2016 5:28 AM | Permalink | Reply to this

Re: HoTT and Philosophy

Are many using slides and then posting them online?

Posted by: David Roberts on September 15, 2016 12:42 PM | Permalink | Reply to this

Re: HoTT and Philosophy

Several used slides, which I gather will be made available.

Steve Awodey read his paper, and presumably could be contacted for a preprint. It takes its departure from that idea of logic as the maximally invariant part of a language. We mentioned one appearance of that idea back here. So HoTT has invariance under equivalence built into it.

Posted by: David Corfield on September 15, 2016 4:42 PM | Permalink | Reply to this

Re: HoTT and Philosophy

Here’s a thought then. I said in my slides that with HoTT the boundary between logic and mathematics is blurred, e.g., we start to find constructions from representation theory built into the calculus, see nLab: infinity-action. And of course there’s all that synthetic homotopy theory, such as here.

With Urs’s addition of the differential cohesion modalities, we start to find the fundamental theorem of calculus, perhaps right up to Noether’s theorem, ‘built in’.

Is there anything interesting to say then about which system produces which mathematics ‘synthetically’? (Long debate about the meaning of that yesterday.) So homotopy groups arise from plain HoTT, the fundamental theorem of calculus from HoTT + certain modalities, etc.

Posted by: David Corfield on September 16, 2016 10:15 AM | Permalink | Reply to this

Re: HoTT and Philosophy

You mean, like maybe some parts of mathematics are “more fundamental” because we have to add less to a foundational theory to get them synthetically? It does seem hard to answer that without knowing what “synthetic” means…

Do we really have the fundamental theorem of calculus from modalities? I thought it was more like skipping over that to get directly to more geometric facts.

Posted by: Mike Shulman on September 16, 2016 11:38 AM | Permalink | Reply to this

Re: HoTT and Philosophy

Yes, that’s the idea. I agree synthetic needs defining, but there could be some kind of ‘reverse mathematics’.

For instance, Felix has coded those results I mentioned using very few conditions on some modalities (was it just a lex idempotent comonad?).

Do we really have the fundamental theorem of calculus from modalities?

I guess we should say that it’s an interpretation of a result of modal HoTT. Anyway that’s how Urs describes Prop 3.18 of Higher prequantum geometry. Convincing?

Posted by: David Corfield on September 16, 2016 12:23 PM | Permalink | Reply to this

Re: HoTT and Philosophy

I have to admit I have never fully grokked all of the stuff that Urs does with cohesion. This is partly my fault for just not finding the time, but I would also appreciate some simple explanations. In particular, Example 3.14 and Proposition 3.17 in that paper could use some proofs, or even intuitive explanations, other than a citation to a 60-page paper. Starting from the basics, for someone who doesn’t live and breath “super”.

Posted by: Mike Shulman on September 16, 2016 5:51 PM | Permalink | Reply to this

Re: HoTT and Philosophy

Yes, a little unpacking would help there, even though it only involves the first row of modalities. So there needs to be an understanding of the differential cohomology diagram, in the context of a specific case, as discussed in section 4 of Differential cohomology theories as sheaves of spectra.

We ought to record him in action more. The vanishing torsion idea came through very clearly at the conference.

I like it when a talk prompts me to have a useful thought just before it becomes needed. So here by slide 17, I was just wondering what reduction of the structure group of the frame bundle to the trivial group would look like, and then that’s what allows canonical GG-structures, and so the notion of flatness.

Posted by: David Corfield on September 17, 2016 10:14 AM | Permalink | Reply to this

Re: HoTT and Philosophy

Just took a moment to look at this a little more. The 60-page paper uses notation that’s fairly impenetrable to me (perhaps it is clearer to people already familiar with differential cohomology), but from a cursory glance it seems that it (1) is about sheaves of chain complexes, not tangent ∞\infty-toposes, (2) uses sheaves on the category of manifolds with corners, not super formal smooth Cartesian spaces, (3) recovers only integration of closed differential forms, (4) recovers only the image of such integration in cohomology, with the connection to integration made visible by a particular point-set-level choice that’s not visible at the homotopy level, and (5) provides no synthetic way to define differential forms, only an abstract construction that happens to agree with integration when specialized to a particular example built out of classically defined differential forms. HPG appears to make stronger claims, but given what I can currently understand, it seems like a stretch to say that the fundamental theorem of calculus arises from modalities. But I would love it if someone could explain why I’m wrong!

Posted by: Mike Shulman on September 22, 2016 10:06 AM | Permalink | Reply to this

Re: HoTT and Philosophy

I would love it if someone could explain why I’m wrong!

Since perhaps the only person in the world who could explain doesn’t frequent these parts, let’s take the request elsewhere.

Posted by: David Corfield on September 22, 2016 12:19 PM | Permalink | Reply to this

Post a New Comment