Conversation
- Assume for now that the colimit of concat is an equivalence - Start on defining the new identity type family over the pushout
Pulling Ben's work
Minor cleanups
jdchristensen
left a comment
jdchristensen
left a comment
There was a problem hiding this comment.
It's great to see this progress!
I'm not sure what you mean about the generalization. We should talk about that in person.
As I was reading it, I couldn't help making style comments. If you can fix those (including in places I didn't label), that'll make it less distracting for me when I review things again.
theories/Basics/Equivalences.v
Outdated
| destruct H as [gf_inv gf_s gf_r gf_adj]. | ||
| destruct H0 as [hg_inv hg_s hg_r hg_adj]. |
There was a problem hiding this comment.
It's best to not refer to variable names generated by Coq, as those can change and cause build failures. So if you want to destruct these, you should name them, e.g. iegf and iehg. But there's normally no need to destruct these, since we can access the components using (-)^-1, eissect, eisretr and eisadj.
That all said, your proof has embedded in it the proof that biinvertibility implies IsEquiv, which is isequiv_biinv in Equiv/BiInv.v. So it would be better to rearrange things so that that result could be used here. Then the proof becomes simple:
apply isequiv_biinv; split; srefine (_; _).
- exact ((h o g)^-1 o h).
- cbn beta. apply eissect.
- exact (f o (g o f)^-1).
- cbn beta. apply (eisretr (g o f)).Not sure how to do the rearranging, though, since BiInv.v depends on a Types.Equiv and Types.Prod. One option would be move part of BiInv.v to Basics/Equivalences.v. (I'm surprised that this hasn't come up before, since it's sometimes easier to use bi-invertibility.)
theories/Basics/Equivalences.v
Outdated
| snrapply cancelR_isequiv. | ||
| - exact B. | ||
| - exact g. | ||
| - exact (two_out_of_six_snd f g h). | ||
| - exact H0. |
There was a problem hiding this comment.
I'd prefer this:
| snrapply cancelR_isequiv. | |
| - exact B. | |
| - exact g. | |
| - exact (two_out_of_six_snd f g h). | |
| - exact H0. | |
| rapply (cancelL_isequiv g). | |
| exact (two_out_of_six_snd f g h). |
or possibly a := one-liner.
theories/Basics/Equivalences.v
Outdated
| split. | ||
| - split. |
There was a problem hiding this comment.
repeat split. is a good idiom to use here. But I would just drop this result, since I doubt it would be used.
| (HQ2 : IsColimit D2 Q2) {T : Type} (t : Q2 -> T) | ||
| : cocone_postcompose HQ1 (t o (functor_colimit m HQ1 HQ2)) | ||
| = cocone_precompose m (cocone_postcompose HQ2 t). | ||
| Proof. |
There was a problem hiding this comment.
The indentation is off here.
There was a problem hiding this comment.
This change to the indentation is wrong. The = was indented correctly before.
However, the Proof. line and the entire proof are indented incorrectly.
theories/PushoutPath/Interleaving.v
Outdated
| - intro C. | ||
| srapply path_cocone. | ||
| + intros n a. simpl. exact (legs_comm C n _ idpath a). | ||
| + intros m n [] a. simpl. | ||
| snrapply (ap (fun x => x @ _) (concat_1p _)). | ||
| - intro C. | ||
| srapply path_cocone. | ||
| + intros n a. simpl. exact (legs_comm C n _ idpath a). | ||
| + intros m n [] a. simpl. | ||
| snrapply (ap (fun x => x @ _) (concat_1p _)). |
There was a problem hiding this comment.
Since the same argument is used twice, I would factor it out as a lemma.
Also, the last line can be replaced with: exact (concat_1p _ @@ 1).
And in the first + bullet, you can avoid introducing a.
theories/PushoutPath/Interleaving.v
Outdated
| snrapply (ap (fun x => x @ _) (concat_1p _)). | ||
| Defined. | ||
|
|
||
| (** The cocone [col_A] induces [idmap : transfinite_A -> transfinite_A]. *) |
There was a problem hiding this comment.
I'd suggest colim_A as the name here. To me, transfinite includes "much larger than countable".
theories/PushoutPath/Interleaving.v
Outdated
| (** We take the colimit of [seq_to_succ_seq] | ||
| and obtain a map [transfinite_A -> transfinite_A] *) | ||
|
|
||
| Definition abstr_colim_seq_to_abstr_colim_succ_seq | ||
| : transfinite_A -> transfinite_A | ||
| := functor_colimit (seq_to_succ_seq A) col_A col_succ. |
There was a problem hiding this comment.
I'm not sure why the rest of this section is here. You've shown that transfinite_A is a colimit. You may want to record the fact that the identity map respects the cones, but other than that, I'm not sure why you want to apply functor_colimit to this situation. And then you spend time showing that the identity map is an equivalence. Maybe this is just leftover code?
(Even if it does turn out to be handy to know that functor_colimit is the identity, the rest of the section doesn't seem to be needed.)
theories/Colimits/Colimit.v
Outdated
| = (functor_colimit (diagram_comp n m) HQ1 HQ3) | ||
| := @equiv_inj _ _ | ||
| = (functor_colimit (diagram_comp n m) HQ1 HQ3) | ||
| := @equiv_inj _ _ |
There was a problem hiding this comment.
The := should be indented to line up with the :, and the = should be two spaces further to the right.
(The same applies to := elsewhere.)
theories/PushoutPath/Interleaving.v
Outdated
| *) | ||
|
|
||
| (** Given the setup above, we want to say that the colimit of the upper lower sequences are the same. *) |
There was a problem hiding this comment.
I think everything in this part should be one long comment instead of closing and restarting comments.
(Elsewhere too.)
| pose (g':=(fun n => f (S n))); | ||
| pose (U':=L); | ||
| pose (L':=(fun n => U (S n))); | ||
| (* Coq can't guess `succ_seq A` here *) | ||
| pose (attempt := (@zigzag_glue_map_tri _ B (succ_seq A) f' g' U' L')). | ||
| pose (attempt:=(@zigzag_glue_map_tri _ B (succ_seq A) f' g' U' L')). |
There was a problem hiding this comment.
I think you can omit parentheses for g', L' and attempt.
|
Everything should now be set for the first learning portfolio. You will find most of our work in PushoutPath.v, Interleaving.v, and GraphQuotientPathInd.v. The first and last file are very much WIP, while Interleaving.v is close to being done. You will find that the comments not just only documents the code, but also contains questions and concerns about the code. This is especially true in GraphQuotientPathInd.v. Here I have choices to make for the 2-cells of the categories I'm defining. I think the choice that I made is incorrect, as can be seen by the aborted code snippet in the end. This file also contains a lot of duplicate code that I don't know if can be optimized. There's also some minor work scattered across Colimit.v and Equivalences.v. There was one more thing, but it is so minor that I cannot remember it. I made a seperate PR for that directly to the Coq-HoTT library. |
3 participants
Hi Dan,
your idea of showing that (cocone_precompose (seq_to_succ_seq A)) is an equivalence simplified everything by a big margin. I was able to prove that the maps I wanted to be equivalences are identities.
I'm not so sure if I should touch this code that much more, I think it is better that I get back to helping Ben with what he is doing right now. However, everything that is inside Section Is_Equiv_colim_succ_seq_to_seq_map can be generalized, and then possibly moved to Colimits.v. This should be very easy.
Another thing is that the 2-out-of-6 property is kind of redundant now, as the equivalences in question are identities. I can instead use isequiv_biinv to build the equivalence. However, I'm a little lazy, and hasn't changed this part of the code.
My naming schemes could also use a little work (we're all looking at you two_out_of_six).
All in all, I'm kinda unsure how useful this piece of code will be for us, so it might just be good to generalize what I can, so it isn't all for naught.