Homotopy Type Theory Electronic Seminar Talks, 2023-12-14
https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html
Joint with Ulrik Buchholtz, Dan Christensen, and Egbert Rijke.
In this talk, we'll construct the tangent sphere bundles on the spheres using an inductive construction, and we'll use this construction to prove the Hairy Ball Theorem. We'll then compute the Euler class of the tangent sphere bundles with an explicit construction. Generalizing from this case, we'll define a preliminary notion of "homotopy manifold" and use an abstract lemma about pushout products to define the product of homotopy manifold structures. This will give us tangent bundles on products of spheres as well. All of this will take place in ordinary book HoTT, and a good deal of it has already been formalized in Coq.