I am trying to build an understanding of the Univalence Axiom in HoTT and I am slightly confused about some definitions.
If I was asked after reading of Chapter 1 of the HoTT book to formulate a definition for the type of equivalences $A \simeq B$, I would write something like this:
$$A \cong B := \sum_{f : A \to B} \sum_{g : B \to A} (f \circ g = 1_{B}) \times (g \circ f = 1_{A})$$
which we might call “naive isomorphism of types”. The author explains that this is not the preferred definition for two reasons:
Functional equality is unnecessary when compared to the a priori weaker notion than pointwise equality (i.e. homotopy), so we replace the $=$ with $\sim$ signs.
That the left and right-inverse necessarily coincide is coincidental and it is equivalent to ask for the left and right-inverse exist independently.
The definition is therefore given as follows:
$$A \simeq B := \sum_{f : A \to B} \left(\sum_{g : B \to A} f \circ g \sim 1_{B}\right) \times \left(\sum_{h : B \to A} h \circ f \sim 1_{A}\right).$$
On the other hand, we know that univalence implies functional extensionality (i.e. the types $f \sim g$ and $f = g$ are equivalent), and it is quite clear that
$$\left(\sum_{g : B \to A} f \circ g \sim 1_{B}\right) \times \left(\sum_{h : B \to A} h \circ f \sim 1_{A}\right) \quad \text{and} \quad \sum_{g : B \to A} (f\circ g \sim 1_{B}) \times(g \circ f \sim 1_A)$$
are equivalent as well (albeit the latter is supposedly less well behaved). The upshot is that $A \cong B$ and $A \simeq B$ are equivalent, under univalence. This leads me to wonder what would go wrong if we took $\cong$ to be the standard notion of equivalence and formulated the Univalence Axiom accordingly. Certainly, for me, the definition of $\cong$ is slightly more intuitive because it is verbatim the same notion as in 1-categories and needs not be motivated by homotopy theory or higher categories. But I'm guessing there is a good reason that things are presented in the way they are.
It turns out that $$ \operatorname{isequiv}(f) \equiv \left( \sum_{g : B \to A} f \circ g \sim 1_{B} \right) \times \left( \sum_{h : B \to A} h \circ f \sim 1_{A} \right) $$ and $$ \operatorname{qinv}(f) \equiv \sum_{g : B \to A} (f \circ g \sim 1_{B}) \times (g \circ f \sim 1_{A}) $$ are not actually equivalent. This is mentioned briefly in Section 2.4, and Chapter 4 gives a proof. More explicitly, Theorem 4.1.3 gives an example of a function $f : A \to B$ such that $\operatorname{qinv}(f)$ is not a mere proposition, while Theorem 4.3.2 proves that $\operatorname{isequiv}(f)$ is a mere proposition. So $\operatorname{isequiv}(f)$ and $\operatorname{qinv}(f)$ cannot be equivalent.