Coinductive Invertibility in Higher Categories

TL;DR

This paper introduces three coinductive notions of invertibility in higher categories, proves their equivalence, and formalizes these results in Agda, advancing the understanding of invertibility in complex categorical structures.

Contribution

It defines three coinductive invertibility notions in higher categories and proves their equivalence, providing a unified framework for invertibility concepts.

Findings

The three notions of invertibility are equivalent in higher categories.

The methods are generic and applicable to various models of higher category theory.

Formalization in Agda confirms the correctness of the proofs.

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.