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