Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2407.10891 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Table of Contents:
- 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.