Coinductive Invertibility in Higher Categories

arXiv2008.10307MaRDI QIDQ6347607FDOQ6347607

Authors: Alex Rice 

Publication date: 24 August 2020

Abstract: 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 $omega$-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.

This page was built for publication: Coinductive Invertibility in Higher Categories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6347607)