Eckmann-Hilton and the Hopf Fibration

This talk presents an improved version of my honors thesis, making essential usage of the notion of a type family equipped with a lift.

Recording of the Talk

Talk Abstract

Slides for the talk

Related materials:

Tom Jack’s cubical code

Confrence website