University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > On bilinearity of Whitehead products in Homotopy Type Theory

On bilinearity of Whitehead products in Homotopy Type Theory

Add to your list(s) Download to your calendar using vCal

  • UserUlrik Buchholtz, University of Nottingham
  • ClockFriday 11 November 2022, 14:00-15:00
  • HouseSS03.

If you have a question about this talk, please contact Jamie Vicary.

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.)

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity