  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.

Category Theory