[[!redirects A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory]] < [[nlab:A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory]] category: redirected to nlab