# Equivalent form of the Univalence Axiom

I'm reading the new HoTT 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?

-
Mike I agree with your choice to retag (abbreviation make terrible tags in most cases), but this tag was hott! :-) –  Asaf Karagila Jun 22 '13 at 17:40

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.

-
Interesting. So how does uniqueness of inverses fail? Specifically, what prevents the type in your displayed equation to be equivalent to my $\mathsf{isisom}(f)$? –  François G. Dorais Jun 22 '13 at 18:04
Have a look at section 4.1. –  Mike Shulman Jun 22 '13 at 18:44
That's what I was reading when I came up with the question! I'm trying to keep my reasoning as informal as possible. Here's a thought... By (ab)using uniqueness of inverses this way I'm losing the path that led me to the equality of left and right inverses and replacing it by $\mathsf{refl}$; that's not cool. Does that capture what is lost in passing from $\mathsf{biinv}(f)$ to $\mathsf{isisom}(f)$. –  François G. Dorais Jun 22 '13 at 19:13
Yes, I think that's more or less correct. Personally, I find 4.1.1 and its proof to be the most compelling explanation, but I have a hard time summing it up in a sentence. –  Mike Shulman Jun 23 '13 at 0:58
I got some more insights in the mistake, which I posted here: dorais.org/archives/1438 –  François G. Dorais Jun 23 '13 at 18:15

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.

-
Very nice to see you here! –  François G. Dorais Jun 23 '13 at 20:56
@Steve, is there any logical reason to prefer $=\simeq \simeq$ over $== \simeq$? They both seem to imply each other, although that requires climbing up the univalence ladder, which is a bit unnerving, but looks solid and innocent. The second form $==\simeq$ looks more logically reasonable to me, since we postulate a logical equality between types, and that notion is built-in into type theory, unlike equivalence, which is geometrically and constructively reasonable, but still something extra. –  Anton Fetisov Oct 17 '13 at 23:53