Clarification of the proof of Lemma 6.2.9. (universal property of the circle)

Question

Clarification of the proof of Lemma 6.2.9. (universal property of the circle)

FernandoChu opened this issue 2 years ago · 10 comments

Here's the proof for easy reference

(In what follows, I've renamed the $f $ in the proof to $\varphi $)

For two fibers $(f , eqf) ,(g , eqg) : fib_{\varphi} (b , l) $ to be equal, we must show $ p: f = g$, which as mentioned can be proven by the uniqueness principle and functional extensionality, and also that $p_* (eqf) = eqg$. I have not been able to show this, though I've shown that it's enough to have (ap φ p)⁻¹ ∙ eqf = eqg.

I'm stuck in this last step, is this what the proof had in mind? or maybe I'm just overcomplicating it.

Answer 1 · 2022-07-07T21:08:28.000Z

I think you're right, this was the intent (and so the invocation of the uniqueness principle is perhaps overly glib). I don't know offhand the best way to do this; probably you could deduce it from the construction of p in the proof of the uniqueness principle.

Answer 2 · 2022-07-22T18:09:17.000Z

I've been thinking about this, and doing path induction on p and eqf in (ap φ p)⁻¹ ∙ eqf = eqg simplifies the goal to refl (φ f) ≡ eqg, which is false, so while the proof should be able to carried out, I'm suspecting it is not possible to carry it out directly, as was implied. Would you welcome PR using the usual bi-invertible maps?

Answer 3 · 2022-07-22T19:39:52.000Z

You would only do path induction on p if you were trying to prove that this equality holds for *all* p, and it makes sense that that wouldn't be true. I meant that you'd need to use the construction of your *specific* p.

…

On Fri, Jul 22, 2022 at 11:09 AM Fernando Chu ***@***.***> wrote: I've been thinking about this, and doing path induction on p and eqf in (ap φ p)⁻¹ ∙ eqf = eqg simplifies the goal to refl (φ f) ≡ eqg, which is false, so while the proof should be able to carried out, I'm suspecting it is not possible to carry it out directly, as was implied. Would you welcome PR using the usual bi-invertible maps? — Reply to this email directly, view it on GitHub <#1123 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAE53SFCZ4RFXLMVWRFUYP3VVLPVPANCNFSM52PQSZKA> . You are receiving this because you commented.Message ID: ***@***.***>

Answer 4 · 2022-09-19T02:27:44.000Z

Thanks, you're right. I've been thinking about this. We can not induct on p but we can induct on eqg, it is also enough to prove it for the case where f and eqf are the ones from recursion, i.e. f is 𝕊¹-rec A b l and eqf is given by pairing refl b with the computation principle of f. With this assumptions, we need

ap φ (funext (𝕊¹-ind-uniq f g (refl b) (𝕊¹-rec-comp A b l))) = eqf

Where 𝕊¹-ind-uniq is the function from Lemma 6.2.8.

This seems true but I see no way to prove this...

Answer 5 · 2022-09-19T04:04:41.000Z

I think it is much easier to prove that this map has a quasi-inverse, and apply adjointification, than to prove directly that it has contractible fibers. Having contractible fibers, like being a half-adjoint equivalence, contains an extra coherence 2-path that makes it a proposition, but which is harder to construct in examples, and I think that's what's causing the pain here.

Answer 6 · 2022-09-19T15:49:39.000Z

Yup I definetely agree, managing 2-paths is still very hard (to me). I suggest again maybe changing to the usual quasi-inverses proof, I can PR if you want.

Answer 7 · 2022-09-19T16:04:58.000Z

Yes, I was going to suggest that once you worked out the details. (I also just formalized it in HoTT/Coq-HoTT#1664.) If you've done it already, I think a PR would be great. Thanks!

Answer 8 · 2022-09-20T02:43:23.000Z

I've just finished it! (I've also formalized it in my agda repo).

I'll be closing this issue :)

Thank you!

Answer 9 · 2022-09-20T03:03:52.000Z

The usual github-y thing to do would be to leave the issue open until the PR is merged.

Answer 10 · 2022-09-20T14:35:35.000Z

Oh I didn't know, thanks for reopening then