高阶范畴中的共归纳可逆性
Coinductive Invertibility in Higher Categories
摘要：
可逆性是范畴论中的一个重要概念。在高阶范畴论中，可逆性的正确概念变得不那么明显，因为额外的相干条件可能成为可逆结构具有所需性质的必要条件。定义了弱$ω$ -范畴的某些性质，这些性质在任何合理的定义中都是成立的.有了这些性质，我们定义了三个概念的启发同伦类型理论的可逆性。这些是准可逆性，其中需要双侧逆，双可逆性，其中给出单独的左逆和右逆，以及半伴随逆，这是具有额外相干条件的准逆。这些定义采用共归纳数据结构的形式。使用共归纳证明，我们能够证明这三个概念都是等价的，因为给定这些可逆性结构中的任何一个，其他的都可以得到。用于这样做的方法是通用的，它是预期的结果应该适用于任何合理的模型高阶范畴论。许多结果的文件已正式在阿格达使用共归纳记录和机械的大小类型。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
