On bilinearity of Whitehead products in Homotopy Type Theory
- ๐ค Speaker: Ulrik Buchholtz, University of Nottingham
- ๐ Date & Time: Friday 11 November 2022, 14:00 - 15:00
- ๐ Venue: SS03
Abstract
I’ll report on some recent work on maps between spheres in univalent foundations (with a formalization in cubical type theory). For the case of 2-spheres, this requires some results about Whitehead products related to the EHP long exact sequence. (This is joint work with Marc Bezem, Pierre Cagne and Nicolai Kraus.) Studying the types of spheres in homotopy type theory also leads to a new definition of Euler classes, and I’ll explain how. (The latter part is joint work with Dan Christensen, David Jaz Myers, Egbert Rijke, and Jarl Taxerรฅs Flaten.)
Series This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Martin's interesting talks
- School of Technology
- SS03
- tcw57โs list
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.
![[Talks.cam]](/static/images/talkslogosmall.gif)

Ulrik Buchholtz, University of Nottingham
Friday 11 November 2022, 14:00-15:00