Egbert Rijke: A higher encode decode method

Note, that we meet at a non-standard time at 17:30. The talk will be given as a part of the Homotopy Type Theory Electronic Seminar.

Abstract: The Postnikov tower of a pointed type X induces a fiber sequence $K(G,n+1) -> |X|_{n+1} -> |X|_n$ for every n, where G is the (n+1)-st homotopy group of X. This fiber sequence suggests a general approach to computations of higher homotopy groups of types, by encoding a family of n-connected (n+1)-truncated types over the type $|X|_n$. While I do not yet have any finished computations of homotopy groups of types via this approach, it does suggest a fruitful line of research with interesting intermediate results.