You Wouldn't Permutahedron

TL;DR

This paper develops formulas for permutahedral coherence relations and explores their geometric and type-theoretic interpretations, aiming to advance understanding of higher associativity structures.

Contribution

It introduces formulas for permutahedral coherence relations and connects geometric transformations with type-theoretic coherence concepts.

Findings

Defined a transformation of permutahedron into a cube

Proposed a semi-simplicial type framework for coherence relations

Suggested potential translation into formal type theory

Abstract

We develop formulas that define permutahedral commutation coherence relations of all orders. To illustrate the result geometrically, we begin by defining a rigid transformation of the $(n+1)$-permutahedron into a $n$-cube of dimensions $1 \times 2 \times \cdots \times n$. With a fictitious assumption, we 'define' the corresponding coherence relations 'up to associativity' as an instance of a semi-simplicial type in the language of Displayed Type Theory. This is not a formal result in type theory, but we expect this to translate into one as soon as the problem of defining associahedral coherences is solved in a type theory with semi-simplicial types. On the other hand, this not-strictly-well-typed definition may be used to produce well-typed formulas in a restricted setting.