Homotopy type theory and synthetic homotopy theory

This talk will be on zoom only!

For zoom details contact: Barthel, Ozornova, Ray, Teichner.

Homotopy type theory is a logical system in which any basic object is interpreted as a kind of space. Accordingly, a proof that two elements of a space are equal corresponds to a path. Since the space of paths between two points is a primitive in the theory, this gives rise to the possibility of doing homotopy theory synthetically, i.e. homotopical constructions are given natively. Moreover, any property or construction gets automatically transported along identifications via paths.

After an informal introduction to the basic language of HoTT, we give an idea of what synthetic homotopy theory looks like in this system, using the principles described above.

Attachment	Size
hott-intro-weinberger.pdf	375.21 KB