What is...homotopy type theory?

Goal.
I would like to tell you a bit about my favorite theorems, ideas or concepts in mathematics and why I like them so much.
This time.
What is...homotopy type theory? Or: HoTT = Ho + TT.
Disclaimer.
Nobody is perfect, and I might have said something silly. If there is any doubt, then please check the references.
Slides.
www.dtubbenhauer.com/youtube.html
TeX files for the presentation.
github.com/dtubbenhauer/My-Te...
Thumbnail.
c4.wallpaperflare.com/wallpap...
d2r55xnwy6nx47.cloudfront.net...
Main discussion.
arxiv.org/abs/2212.11082
web.archive.org/web/201707070...
www.ams.org/notices/201309/rn...
en.wikipedia.org/wiki/Homotop...
homotopytypetheory.org/book/
en.wikipedia.org/wiki/Homotop...
en.wikipedia.org/wiki/Higher_...
ncatlab.org/nlab/show/homotop...
homotopytypetheory.org/
golem.ph.utexas.edu/category/...
Background material.
en.wikipedia.org/wiki/Foundat...
en.wikipedia.org/wiki/Univale...
en.wikipedia.org/wiki/Intuiti...
en.wikipedia.org/wiki/Proof_a...
en.wikipedia.org/wiki/Automat...
en.wikipedia.org/wiki/Intuiti...
en.wikipedia.org/wiki/Mathema...
en.wikipedia.org/wiki/Structu...)
en.wikipedia.org/wiki/%E2%88%...
en.wikipedia.org/wiki/Simplic...
github.com/HoTT/Coq-HoTT
Computer talk.
github.com/thehottgame/TheHoT...
math.stackexchange.com/questi...
Pictures used.
Picture from • What is...homotopy?
uploads-ssl.webflow.com/5b1d4...
i.stack.imgur.com/3e0fj.png
Pictures from en.wikipedia.org/wiki/Homotop...
Picture from • What is...homotopy of ...
d2r55xnwy6nx47.cloudfront.net...
KZbin and co.
video.ias.edu/univalent/awodey
• Homotopy Type Theory D...
• Video
#categorytheory
#topology
#mathematics

[@alexgryzlov]

Another cool (potential) area that intersects with HoTT is, as far as I know, group theory - since equalities are always required to be invertible, you can use them to encode group-theoretical machinery in higher dimensions.

[@kylerivelli]

That's great intuition. HoTT types are interpreted as (∞,1)-groupoids, where the elements of a type represent objects, and the paths between elements represent morphisms and higher morphisms.

[@VisualMath]

Yes, that is a good observation. I do not know much about this, but certainly people have worked on this and are working one this. See for example: arxiv.org/abs/1802.04315

[@dr-evil]

Thank you for the video. The topic wasn't really too hard. Cheers

[@VisualMath]

Welcome. I am glad that you liked the video! I realized that the essence of HoTT is not difficult to explain, hence the video. Being in the intersection of logic, computer science, topology and category theory certainly doesn’t make HoTT a bestseller, but I buy it anytime ;-)

[@alejandromelo8245]

Wonderful video. Truly, an exciting new mathematical area (at least, for me) to explore.

[@VisualMath]

Careful: HoTT is a rabbit hole 😅 Anyway, I am glad that you liked the video and the topic.

[@pseudolullus]

The video was pretty clear, and exciting

[@VisualMath]

Thanks for the feedback! HoTT is indeed exciting, I hope you like it!

[@pseudolullus]

@@VisualMath I work in computational neuroscience, so all topics covering topology, computation by wholes vs parts, algebraic topology and/or logic are especially interesting (!)

[@VisualMath]

@@pseudolullus I think one of the most amazing things is when different fields come together, say neuroscience and topological data analysis. You are very welcome here and I hope you enjoy it!

[@Jaylooker]

Homotopy type theory may be a good place to attack Whitehead’s algebraic homotopy program. His program suggests there is a construction of an algebraic theory equivalent to a homotopy theory. HoTT involves homotopic paths and ∞-groupoids. Maybe there is some equivalent way to describe a group using homopty theory like I am hoping?

[@VisualMath]

I guess you are referring to this, see ncatlab.org/nlab/show/algebraic+homotopy: [In their talk at the 1950 ICM in Harvard, Henry Whitehead introduced the idea of algebraic homotopy theory and said “The ultimate aim of algebraic homotopy is to construct a purely algebraic theory, which is equivalent to homotopy theory in the same sort of way that ‘analytic’ is equivalent to ‘pure’ projective geometry.” etc.] HoTT and homotopy theory are married, by birth I guess. As far as I can tell 90% of the flow goes HT → HoTT, the other way around is mostly about proof verification and friends. This is extremely exciting(!) and might be the starting point of formalizing HT. Yes, I think you are right. I haven’t seen a formal treatment of Whitehead’s program in HoTT, but certainly there are some things have been done: ncatlab.org/nlab/show/HoTT+methods+for+homotopy+theorists

[@Jaylooker]

@@VisualMath I was referencing that. At least for groups they have Cayley graphs which can be built using a group’s presentation G = with S generators and R relations. Graphs are an example of a simplicial object. Simplicial objects can be used to homotopy theory. Treating Cayley graphs as some form of types is what I’m after. For example, if two groups elements a and b equal each other a = b, there is a path in the Cayley graph between them as if the group elements were types.

[@VisualMath]

@@Jaylooker I like that observation, thanks for sharing!

[@Jaylooker]

@@VisualMath Yup 👍

[@M0rph1sm]

CW complexes retract nicely onto a sub complex….!! Yay Xournal! Ctrl+shift+f

[@VisualMath]

No, I am fancy. Its Xournal++ 🤣

[@diek_yt]

Great video. Keep it up!!

[@VisualMath]

"Keep it up!!" Thanks, I will try my best. We will see how that goes 😅 Anyway, I hope you enjoy math 👍

[@alieser7770]

Sir, you are incredible

[@VisualMath]

Haha, clearly not. But thanks for watching and commenting 😀 P.S.: I go by they/them so sir is not much appreciated. Its fine, no worries.

[@leihaochen709]

Can I ask a question? You said HoTT can potentially make automated proof system. Is this system able to prove all the theorems in mathematics or only theorems in homotopy theory?

[@VisualMath]

Excellent question! HoTT is an alternative foundation that is based on concepts from topology and type theory. It avoids the need for ZFC set theory and some of its troublesome axioms. As such it should be able to formalize “everything”, also via computer. On the other hand, since HoTT is based on topology, it is however not surprising that the key examples of computer verification via HoTT are within topology.

[@leihaochen709]

@@VisualMath Thank you for the helpful reply!

[@VisualMath]

@@leihaochen709 You are very welcome!

[@biblebot3947]

@@leihaochen709I believe it’s possible to make a model of ZFC in HoTT, so theoretically, you could just recreate all the proofs in HoTT

[@axog9776]

you are beautiful

[@VisualMath]

Very questionable ;-)

[@rhodesmusicofficial]

​@@VisualMathNOT questionable 😤

[@VisualMath]

@@rhodesmusicofficial No, I can go for a formal proof is you want ;-)