Quasi-Inverse

Definition

Let $f:A\to B$. The type of quasi-inverses (often denoted qinv) corresponds to the classical homotopy definition:

$$\mathsf{qinv}(f):\equiv \sum _{g:B\to A}((f\circ g\sim {\mathsf{id}}_B)\times (g\circ f\sim {\mathsf{id}}_A))$$

This type contains the data of the inverse and the homotopies.

This is precisely the isomorphisms in the homotopy category.

Distinction from equivalence in HoTT

While logically equivalent (one is inhabited iff the other is), they differ in Homotopy Levels:

1. $\mathsf{isEquiv}(f)$ is always a proposition ($(-1)$-type).
2. $\mathsf{qinv}(f)$ is generally not a proposition (it allows multiple distinct coherence structures).

Relation

We have a logic equivalence:

$$\mathsf{qinv}(f)\leftrightarrow \mathsf{isEquiv}(f)$$

However, to ensure $\mathsf{id}\to \mathsf{Equiv}$ is an embedding, we define $A\simeq B$ using $\mathsf{isEquiv}$.

An alternative “correct” definition is half-adjoint equivalence, which augments qinv with a coherence condition to make it a proposition.