Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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?

share|improve this question
2  
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
add comment

2 Answers 2

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.

share|improve this answer
    
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
1  
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
1  
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
add comment

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.

share|improve this answer
4  
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
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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