一句话：用 Agda 证明 parity complexes 不满足自由性，并提出满足自由性的修正形式化。
在严格 ω-范畴研究中，pasting diagram 应描述由其中 cell 自由生成的 ω-范畴，但一般地刻画这一概念十分困难。已有定义中，parity complexes 以 cell 集合表示边界，较为易计算。本文首先在 Agda 中机器化证明 parity complexes 并不满足所期望的自由性，从而表明其不能正确描述自由 ω-范畴。随后，作者提出一种新的形式化，可视为 parity complexes 的修正版本，并满足自由性性质。关键结果是识别出 parity complexes 的缺陷，并给出既保留可计算性又正确描述自由 ω-范畴的替代结构。
The notion of pasting diagram is central in the study of strict ω -categories: it encodes a collection of morphisms for which the composition is defined unambiguously. As such, we expect that a pasting diagram itself describes an ω-category which is freely generated by the cells constituting it. In practice, it seems very difficult to characterize this notion in full generality and various definitions have been proposed with the aim of being reasonably easy to compute with, and including common examples (e.g. cubes or orientals). One of the most tractable such structure is parity complexes, which uses sets of cells in order to represent the boundaries of a cell. In this work, we first show that parity complexes do not satisfy the aforementioned freeness property by providing a mechanized proof in Agda. Then, we propose a new formalism that satisfies the freeness property and which can be seen as a corrected version of parity complexes.
DOI 原文 ·
@inproceedings{paperbot5017,
title = {Describing free $\omega$ -categories},
author = {Simon Forest and Samuel Mimram},
booktitle = {LICS},
year = {2019},
doi = {10.1109/lics.2019.8785687}
}