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?

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

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.


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.

  • $\begingroup$ 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)$? $\endgroup$ – François G. Dorais Jun 22 '13 at 18:04
  • 1
    $\begingroup$ Have a look at section 4.1. $\endgroup$ – Mike Shulman Jun 22 '13 at 18:44
  • 1
    $\begingroup$ 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)$. $\endgroup$ – François G. Dorais Jun 22 '13 at 19:13
  • $\begingroup$ 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. $\endgroup$ – Mike Shulman Jun 23 '13 at 0:58
  • 2
    $\begingroup$ I got some more insights in the mistake, which I posted here: dorais.org/archives/1438 $\endgroup$ – 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.

  • 4
    $\begingroup$ Very nice to see you here! $\endgroup$ – François G. Dorais Jun 23 '13 at 20:56
  • $\begingroup$ @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. $\endgroup$ – Anton Fetisov Oct 17 '13 at 23:53
  • 3
    $\begingroup$ @AntonFetisov Very belated answer, but in fact neither $(A=B)\simeq (A\simeq B)$ or $(A=B)=(A\simeq B)$ is 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 form $(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. This seems a bit more of a stretch with $(A=B)=(A\simeq B)$, although I suppose not if we've fully internalized univalence. (-: $\endgroup$ – Mike Shulman Jan 2 '18 at 18:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.