Flattening lemma for GraphQuotient #1851
Conversation
Signed-off-by: Ali Caglayan <[email protected]>
|
Glad to see this! Is it ok if I push a change that mainly updates comments? There are some that I think add more clutter than help which I'd like to condense or delete, and it's a bit tedious to suggest many changes via the github ui. |
|
@jdchristensen Feel free to push to this PR! |
|
The failing check just looks like a network glitch again. I'll restart it when the CI lets me. |
|
Now it's an error about missing artifacts. We can ignore it. |
|
@jdchristensen I've rerun the jobs when it finishes I will merge. |
|
Oh, I had one other comment. Do you think the flattening lemma should be put in a separate file, GraphQuotient_Flattening.v? This might help with dependencies, so only files that use flattening will need the extra dependencies. |
| rewrite 3 concat_pp_p. | ||
| apply moveR_Vp. | ||
| rewrite (ap10_dpath_arrow DGraphQuotient (fun _ => Q) (gqglue s)). | ||
| hott_simpl. |
There was a problem hiding this comment.
Is it hard to replace the hott_simpl with something more direct? It is a bit slow and also makes the Defined slow because it makes the proof term large.
There was a problem hiding this comment.
I'll see about doing that, just laziness on my part.
There was a problem hiding this comment.
I'll do it in a follow up PR so I don't have to pull the changes here again.
BTW, I'm not sure why this folder uses underscores in names. Besides the Classes library, the only other files with an underscore are two files in HIT. |
I don't think there is any gain in keeping them separate. The flattening lemma for graph quotients doesn't pull that much in and I think it's better organised to have each HITs flattening lemma in hand. When we use the results it can be useful to have them in one place. |
Underscores are a historical artefact so I generally don't introduce them. There are times when they are needed, i.e. when naming files which have punctuation in their title. |
Co-authored-by: Dan Christensen <[email protected]>
Well, more than half of the library depends on the existing material in GraphQuotient.v, while only 7 files currently depend on the flattening lemma for colimits. So it's important that the existing results in GraphQuotient get built early. I might not push for this, except that we already split out the flattening lemmas for the other colimits, so it would be natural to continue that. |
|
@jdchristensen What about splitting the various HITs into files like we do for Join? That way we can have the core definition and various results like functionality or flattening in separate files? In any case, I would suggest doing the splitting later when we have the flattening lemmas and we can do it all in one go. |
In this PR we state and prove the flattening lemma for [GraphQuotient] which grants #1833. This is much more direct than other flattening lemmas we have in the library and might lead to better computation.
I'm working on deriving flattening lemmas for coequalizers and pushouts after this. Lot's of exciting stuff after that!
I took the time to explain some of the ideas that go into this proof as it can be quite instructive. Hopefully it reads OK and will be useful to future eyes. I wanted to emphasise how its quite an important consequence of univalence as it makes theory inside a higher topos happen.
@mikeshulman I've also added you as a reviewer so that you can give me feedback about the comments I've written. If you are too busy however that's no problem.