Modern Physics Formalized in Modal Homotopy Type Theory by Urs Schreiber

Talk at: FOMUS 2016. For all Talks and more information, slides etc. see: fomus.weebly.com/
Modern Physics Formalized in Modal Homotopy Type Theory by Urs Schreiber
Please note: This is a reupload due to a wrong caption
Abstract: Homotopy type theory is argued to have semantics in infinity-toposes. Under this translation, modal operators are interpreted as idempotent infinity-(co-)monads. Remarkably, a simple progression of adjoint idempotent infinity-(co-)monads on an infinity-topos ("differential cohesion") provides enough structure to elegantly axiomatize large fragments of modern physics: pre-quantum local variational field theory, Noether's theorem, BPS charges, etc. Hence all of this lends itself to synthetic formalization in HoTT. The talk gives a survey of the relevant cohesive infinity-topos theory and of the first steps of formalizing it in HoTT, due to Shulman and Wellen.
This workshop was organised with the generous support of the Association for Symbolic Logic (ASL), the Association of German Mathematicians (DMV), the Berlin Mathematical School (BMS), the Center of Interdisciplinary Research (ZiF), the Deutsche Vereinigung für Mathematische Logik und für Grundlagenforschung der Exakten Wissenschaften (DVMLG), the German Academic Merit Foundation (Stipendiaten machen Programm), the Fachbereich Grundlagen der Informatik of the German Informatics Society (GI) and the German Society for Analytic Philosophy (GAP).

[@mkaeterna9161]

Lawvere and Hegel would be proud of this most shocking application of dialectical philosophy.

[@NoNTr1v1aL]

Absolutely amazing video!

[@janee4826]

Hey Urs, ich versteh kein Wort- kannste mir das nochmal erklären?

[@GeorgWilde]

Sie konnen click subtitles - automatic translation.