## Abstract

A combinatorial theory of associative n-categories has recently been proposed, with strictly associative and unital composition in all dimensions, and the weak structure arising as a notion of ‘homotopy’ with a natural geometrical interpretation. Such a theory has the potential to serve as an attractive foundation for a computer proof assistant for higher category theory, since it allows composites to be uniquely described, and relieves proofs from the bureaucracy of associators, unitors and their coherence. However, this basic theory lacks a high-level way to construct homotopies, which would be intractable to build directly in complex situations; it is not therefore immediately amenable to implementation.

We tackle this problem by describing a ‘contraction’ operation, which algorithmically constructs complex homotopies that reduce the lengths of composite terms. This contraction procedure allows building of nontrivial proofs by repeatedly contracting subterms, and also allows the contraction of those proofs themselves, yielding in some cases single-step witnesses for complex homotopies. We prove correctness of this procedure by showing that it lifts connected colimits from a base category to a category of zigzags, a procedure which is then iterated to yield a contraction mechanism in any dimension. We also present homotopy.io, an online proof assistant that implements the theory of associative n-categories, and use it to construct a range of examples that illustrate this new contraction mechanism.

We tackle this problem by describing a ‘contraction’ operation, which algorithmically constructs complex homotopies that reduce the lengths of composite terms. This contraction procedure allows building of nontrivial proofs by repeatedly contracting subterms, and also allows the contraction of those proofs themselves, yielding in some cases single-step witnesses for complex homotopies. We prove correctness of this procedure by showing that it lifts connected colimits from a base category to a category of zigzags, a procedure which is then iterated to yield a contraction mechanism in any dimension. We also present homotopy.io, an online proof assistant that implements the theory of associative n-categories, and use it to construct a range of examples that illustrate this new contraction mechanism.

Original language | English |
---|---|

Title of host publication | 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |

Publisher | IEEE Xplore |

Pages | 1-13 |

Number of pages | 13 |

ISBN (Electronic) | 978-1-7281-3608-0, 978-1-7281-3607-3 |

ISBN (Print) | 978-1-7281-3609-7 |

DOIs | |

Publication status | Published - 5 Aug 2019 |

Event | Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019) - Vancouver, Canada Duration: 24 Jun 2019 → 27 Jun 2019 |

### Conference

Conference | Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019) |
---|---|

Country/Territory | Canada |

City | Vancouver |

Period | 24/06/19 → 27/06/19 |

## Keywords

- wires
- tools
- calculus
- standards
- coherence
- buildings
- computer science

## Fingerprint

Dive into the research topics of 'High-level methods for homotopy construction in associative*n*-categories'. Together they form a unique fingerprint.