Homotopy Type Theory is often referred to informally as the internal
language of higher category theory. This slogan can be made precise, and I
will state and explain the corresponding conjectures. Afterwards, I will
report on the progress towards proving these conjectures.
Links:
[1] https://www.mpim-bonn.mpg.de/de/taxonomy/term/39
[2] https://www.mpim-bonn.mpg.de/de/node/3444
[3] https://www.mpim-bonn.mpg.de/de/node/6459