Quantum Mathematics Seminar: Egbert Rijke (University of Ljubljana)

Quantum Mathematics Seminar, external speaker:

Speaker: Egbert Rijke (University of Ljubljana)

Title: Universal properties of truncations

Abstract: It is often difficult to compute homotopy groups of types in homotopy type theory, just as in algebraic topology. One approach to compute homotopy groups of types is via the postnikov tower, which consists of fiber sequences K(G,n+1) -> ||X||_{​​​n+1}​​​ -> ||X||_n, where the type ||X||_k is the k-truncation of the type X and G is the (n+1)-st homotopy group of X. In other words, we can compute homotopy groups by manually defining these fiber sequences. In order to do this, we need to define a map ||X||_n -> U into the universe of all Eilenberg-Mac Lane spaces K(G,n+1). This requires new elimination principles for the truncation, that generalize previous results of Kraus. I will present some ideas on this topic, but it is still work in progress.

One hour talk, followed by informal discussion.

All are welcome. Please contact the seminar organizer to be added to the talk.