论文标题
高等类别的共同体可逆性
Coinductive Invertibility in Higher Categories
论文作者
论文摘要
可逆性是类别理论中的重要概念。在较高的类别理论中，不可逆转性的正确概念是什么，因为可逆结构具有所需的特性是必要的。我们定义了一些我们期望在弱$ω$类别的任何合理定义中持有的某些属性。使用这些属性，我们定义了受同义类型理论启发的三个不可逆转概念。这些是准稳定性，其中需要两面逆，双向可逆性，在其中给出了单独的左和右逆，而半偶会逆，这是具有额外相干条件的准内属。这些定义采用共同诱导数据结构的形式。使用共同的证据，我们能够证明这三个概念都是等效的，因为可以获得这些可逆性结构中的任何一种，可以获得其他概念。用于执行此操作的方法是通用的，预计结果应适用于任何合理的高级理论模型。本文的许多结果已在AGDA中使用共同诱导记录和大小类型的机械进行了形式。
Invertibility is an important concept in category theory. In higher category theory, it becomes less obvious what the correct notion of invertibility is, as extra coherence conditions can become necessary for invertible structures to have desirable properties. We define some properties we expect to hold in any reasonable definition of a weak $ω$-category. With these properties we define three notions of invertibility inspired by homotopy type theory. These are quasi-invertibility, where a two sided inverse is required, bi-invertibility, where a separate left and right inverse is given, and half-adjoint inverse, which is a quasi-inverse with an extra coherence condition. These definitions take the form of coinductive data structures. Using coinductive proofs we are able to show that these three notions are all equivalent in that given any one of these invertibility structures, the others can be obtained. The methods used to do this are generic and it is expected that the results should be applicable to any reasonable model of higher category theory. Many of the results of the paper have been formalised in Agda using coinductive records and the machinery of sized types.
