Flattening lemma for GraphQuotient about coq-hott

[jdchristensen]

Without the flattening lemma, we cannot describe the total space of the Hopf fibration and relate it to a join.

We have HIT/Flattening.v which seems to handle coequalizers, and Colimits/Colimit_Flattening.v which seems to handle arbitrary colimits (indexed by a graph). Then Colimits/Colimit_Pushout_Flattening.v which deduces the flattening lemma for pushouts from the one for general colimits. The first two seem redundant, and I don't know why both exist. In any case, all we need are pushouts for the Hopf fibration, so I think we should be good, right?

[Alizter]

@jdchristensen The first is from 10 years ago and was from when Coeq was the HIT that was used to define others. The second is for the Type valued diagram Colimit library and I adapted that to use Coeq IIRC. I'm suggesteing we state the flattening lemma for GraphQuotient and from that all flattening lemmas can be derived.

Also, the first flattening lemma proof we have uses a HIT for the sigma type of the family, and AFAIK this is an unnecessary step as most HIT describe their own flattening lemma HIT by proving the induction principle it should have.

Therefore having the flattening lemma for GraphQuotients will be useful to derive them for all of them.

I believe a higher level idea of what is happening is that we are producing "lax colimits" in the Grothendieck category. Therefore it might be possible to leverage some idea of "displayed colimit" and show that Type can turn displayed colimits into colimits in the Grothendieck category. This should be a "descent property" that is found in all oo-topoi and probably other categories like pType, Spectra and 1-categories.

Since we dont yet have an idea of what colimits will look like nevermind displayed colimits, its probably not worth doing this with the wildcat library just yet. Althoigh, descent for pushouts will be very useful for producing things like the Hilton-Milnor milnor splitting.

[jdchristensen]

Makes sense. But about the specific question I asked, we do currently have what we need to determine the total space of the Hopf fibration, don't we?

[Alizter]

@jdchristensen Yes, specifically about the total space of the Hopf fibration, we are missing the flattening lemma for pushouts. The one for Coequalizers can be used, but I am not fond of having to go through the HIT there. The one for Colimits can also be used but we have to pass along the equivalence with our pushouts which is not desirable. Therefore, in my mind, it makes sense to do flattening for GraphQuotients and derive all the others as needed.

FTR it is possible (or more rather has been done) to do flattening for graph quotients, Floris wrote them out for lean: https://github.com/leanprover/lean2/blob/master/hott/hit/quotient.hlean

[jdchristensen]

We do have flattening for pushouts in Colimits/Colimit_Pushout_Flattening.v. But is your point that these aren't identical to the pushouts defined in Colimits/Pushout.v? They are equivalent, which should hopefully be enough. (I agree with you that unify all of this would be great, I'm just having trouble understanding what we are missing for the Hopf fibration.)

[Alizter]

@jdchristensen Yes, my point is that it requires passing back and forth the equivalence and I would rather have a more direct lemma. Strictly speaking you are correct, there is nothing blocking the total space for Hopf fibration.