Equivalent form of the Univalence Axiom

You've made two changes in going from $\mathsf{isequiv}(f)$ to your "$\mathsf{isisom}(f)$": you replaced homotopy $\sim$ by equality $=$ (justified by function extensionality), and you condensed the left and right inverses $g$ and $h$ into a single inverse (not justified). Thus, your "$\mathsf{isisom}(f)$" is not equivalent to $\mathsf{isequiv}(f)$ but rather to what we in the book called $\mathsf{qinv}(f)$, the type of quasi-inverses of $f$. The two are logically equivalent, i.e. there are maps in both directions, but they are not equivalent types. Thus, the univalence axiom does not even imply that $A=B$ is equivalent to your "$A\cong B$" — in fact, it contradicts it. See sections 2.4, 4.1, and the rest of chapter 4.

If you made only the first change, replacing $\sim$ by $=$ but keeping $g$ and $h$ separate, then it would be true (by function extensionality) that $\mathsf{isequiv}(f)$ is equivalent to

$$ \Big(\sum_{g:B\to A}(f\circ g = \mathsf{id}_B)\Big) \times \Big(\sum_{h:B\to A}(h\circ f = \mathsf{id}_A)\Big), $$

With this change, I think the rest of your reasoning is correct.


A nice thing about the usual formulation of UA in the form $(A = B)\simeq (A\simeq B)$ is that it implies $(A = B) = (A\simeq B)$, by UA one universe up.


Still not an answer to the second question, but I wanted to add something else that's missing: in fact the bare statement $(A=B)\simeq (A\simeq B)$ is not known to be a correct form of the univalence axiom. The correct statement is that the canonical map $(A=B) \to (A\simeq B)$ is an equivalence. The statement $(A=B)\simeq (A\simeq B)$ can be regarded as an abusive abbreviation of this, in the same way that mathematicians often write "$A\cong B$" to mean that some canonical map $A\to B$ is an isomorphism, but to be precise we have to be careful.

There is now a much weaker-looking known equivalent form of the univalence axiom, see here. However, it does still use pointwise homotopies in the equivalences that are to be made into equalities. I suspect that the corrected form "the canonical map $(A=B) \to (A\cong B)$" of your second question is indeed strictly weaker than univalence in the absence of funext, but I don't know.