In mathematics, the first Blakers–Massey theorem, named after Albert Blakers and William S. Massey,[1][2][3] gave vanishing conditions for certain triad homotopy groups of spaces.
However the third paper of Blakers and Massey in this area[4] determines the critical, i.e., first non-zero, triad homotopy group as a tensor product, under a number of assumptions, including some simple connectivity.
[5] The triad connectivity result can be expressed in a number of other ways, for example, it says that the pushout square above behaves like a homotopy pullback up to dimension
The generalization of the connectivity part of the theorem from traditional homotopy theory to any other infinity-topos with an infinity-site of definition was given by Charles Rezk in 2010.
[6] In 2013 a fairly short, fully formal proof using homotopy type theory as a mathematical foundation and an Agda variant as a proof assistant was announced by Peter LeFanu Lumsdaine;[7] this became Theorem 8.10.2 of Homotopy Type Theory – Univalent Foundations of Mathematics.