## Abstract

This paper contributes to recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory. We present a mechanized proof of a result called the Blakers-Massey connectivity theorem, which relates the higher-dimensional loop structures of two spaces sharing a common part (represented by a pushout type, which is a generalization of a disjoint sum type) to those of the common part itself. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which was used in previous formalizations. The proof is more direct than existing ones that apply in general category-theoretic settings for homotopy theory, and its mechanization is concise and high-level, due to novel combinations of ideas from homotopy theory and from type theory.

Original language | English (US) |
---|---|

Title of host publication | Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016 |

Publisher | Institute of Electrical and Electronics Engineers Inc. |

Pages | 565-574 |

Number of pages | 10 |

ISBN (Electronic) | 9781450343916 |

DOIs | |

State | Published - Jul 5 2016 |

Externally published | Yes |

Event | 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 - New York, United States Duration: Jul 5 2016 → Jul 8 2016 |

### Publication series

Name | Proceedings - Symposium on Logic in Computer Science |
---|---|

Volume | 05-08-July-2016 |

ISSN (Print) | 1043-6871 |

### Conference

Conference | 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 |
---|---|

Country/Territory | United States |

City | New York |

Period | 7/5/16 → 7/8/16 |

### Bibliographical note

Publisher Copyright:© 2016 ACM.