Dan Christensen: Manifolds in Homotopy Type Theory

[Please note the unusual time & place of the seminar, we are meeting on Tuesday in room 3.06.]

Speaker: Dan Christensen (University of Western Ontario, Canada)

Abstract: I will discuss work in progress on describing manifolds using the language of homotopy type theory. I will begin by reviewing some background material on (homotopy) pushouts and their description using higher inductive types, and will talk about the special cases of the suspension of a type and the join of two types, both of which lead us to spheres. Then I will present a definition of (homotopy) n-manifold in HoTT and give motivation for the definition. I will end by sketching two new results: a proof that the product of two manifolds is a manifold, and a proof that the spheres have manifold structures.

The talk will be informal, and I'll not assume very much background in HoTT.