[analytiqhub]

Homotopy type theory is definitely the way to go. This 2016 talk from Vladimir Voevodsky is a good entrypoint for the general audience:

https://www.youtube.com/watch?v=gOBqROtRoPA