A cubical Squier's theorem

Maxime Lucas (1, 2)

1 IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
2 PI.R2 - Design, study and implementation of languages for proofs and programs

The homotopical Squier's theorem relates rewriting properties of a presentation of a monoid with homotopical invariants of this monoid. Lately, this theorem has been extended, enabling one to build a so-called polygraphic resolution of a monoid starting from a presentation with suitable rewriting properties. It is currently a work in progress to get a better understanding of these results. We argue that cubical categories are a more natural setting in which to express and possibly extend those results. As a proof-of-concept, we give in this paper a new proof of Squier's homotopical theorem using cubical categories.

Domaines: Topologie algébrique [math.AT]; Catégories et ensembles [math.CT]; Logique en informatique [cs.LO]

Maxime Lucas. A cubical Squier's theorem. 2017. ⟨hal-01662132⟩