I'm reading the new [HoTT book](http://homotopytypetheory.org/book/) and I'm wondering about a potential equivalent form of the Univalence Axiom: $(A \simeq B) \simeq (A = B)$.


For simplicity, I'm tacitly working in a fixed universe. It is known that the univalence axiom implies function extensionality $$\mathsf{funext}:(f \sim g) \to (f = g)$$ where $f,g$ are from the dependent product type $\prod\_{x:A} B(x)$ and $$(f \sim g) :\equiv {\textstyle\prod\_{x:A} (f(x) = g(x))}$$ is the type of homotopies from $f$ to $g$. 


Assuming this, it seems that 
$$\mathsf{isequiv}(f) :\equiv \Big(\sum\_{g:B\to A} (f \circ g \sim \mathsf{id}\_B)\Big) \times \Big(\sum\_{h:B\to A} (h \circ f \sim \mathsf{id}\_A)\Big)$$
boils down to saying that $f$ is an isomorphism:
$$\mathsf{isisom}(f) :\equiv \sum\_{g:B\to A} (f \circ g = \mathsf{id}\_B)\times(g \circ f = \mathsf{id}\_A).$$
Therefore, still assuming function extensionality, there is an equivalence between equivalence $$A \simeq B :\equiv \sum\_{f:A \to B} \mathsf{isequiv}(f)$$ and isomorphism $$A \cong B :\equiv \sum\_{f:A \to B} \mathsf{isisom}(f).$$


Assuming that the above is correct, the Univalence Axiom should be equivalent to the conjunction of functional extensionality with the weaker statement: $(A \cong B) \simeq (A = B)$. I like this conceptual splitting of the Univalence Axiom. Is the above correct or is there a flaw in my informal reasoning? Is it known that $(A \cong B) \simeq (A = B)$ is weaker than the Univalence Axiom?




---


As Mike pointed out in his answer, the correct definition of $A \cong B$ should be $$A \cong B :\equiv \sum\_{f:A \to B} \mathsf{biinv}(f)$$ where $$\mathsf{biinv}(f) :\equiv \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 revised definition, it does appear to be the case that the Univalence Axiom splits into function extensionality and the formally weaker $(A \cong B) \simeq (A = B)$. The second question above should be corrected with this new formulation in mind: is $(A \cong B) \simeq (A = B)$ actually weaker than the Univalence Axiom?



Equivalent form of the Univalence Axiom
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](https://ncatlab.org/nlab/show/univalence+axiom#WeakerEquivalentForms). 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.


