Refactor properties of lifts of families out of 26-descent

[VojtechStep]

The file consisted of two sections: proof that the pullback property of pushouts implies the dependent pullback property of pushouts (with some infrastructure for lifts of families of elements), and characterization of families over pushouts via descent data for pushouts.

The plan is to refactor the first part into more appropriate locations throughout the library.

[EgbertRijke]

Since these checks pass it is probably best if we merge this PR, because I’m getting into the territory of this PR with my spans pr

[VojtechStep]

I think it's a good idea to split this PR in two, one for the dependent-pullback-property<->pullback-property refactor, and one for the descent data refactor.

Unfortunately I still have to port and add some prose for the first part, and I don't know when I'll get back to working on this, so I guess feel free to wreak havoc on 26-descent, since in the end it will be deleted.

I'm okay with holding this PR and resolving conflicts after the spans PR is merged.

[EgbertRijke]

I’m working through all these files right now because the spans PR makes such fundamental changes to how pushouts work

[EgbertRijke]

My PR is changing every line of code in 26-descent. This probably means that there is no sensible way to resolve merge conflicts other than doing the work again that you have already been doing. So I'm going to try to do the work that you have been doing in this PR in my spans PR, and give 26-descent a thorough refactor. My apologies for the complications.

[EgbertRijke]

I’m not sure it is wise to keep working on this pull request. It would be better to tell me what you want to change so that I can do it in spans

[VojtechStep]

I looked at Spans and it doesn't look like you changed the parts of 26-descent that deal with lifts (understandably, since they don't interact with spans directly), so I thought I'd restrict this PR to moving that into more appropriate places in the library, and add some prose in the process so that I understand it better (my main motivation is that I want to be able to properly explain the intuition behind pullback-property -> dependent-pullback-property, since I don't really "get it").

AFAICT the intersection of this PR and Spans is that I just moved pullback-property-dependent-pullback-property-pushout, cone-family-dependent-pullback-property, is-pullback-cone-family-dependent-pullback-family and dependent-pullback-property-pullback-property-pushout to synthetic-homotopy-theory.dependent-pullback-property-pushouts, so would it be possible to keep this open and merge it before Spans, and then do the span thing in that file?

[EgbertRijke]

Yep that’s definitely possible. I’ll limit my work on 26-decent for the time being. Thanks for the heads up

[VojtechStep]

This one is ready for review

[VojtechStep]

I added a table on the different conditions equivalent to "being a pushout", but I didn't include it in more places, because I wanted to reduce the amount of conflicts with #885

[EgbertRijke]

Well done! That was a very nontrivial thing to refactor.

[EgbertRijke]

Since @VojtechStep has exams and this PR is crucial for our current refactoring efforts of synthetic homotopy theory, I'm thinking about merging this PR without the review comments being addressed. In that case I would address the review comments myself in #885. Would this be an acceptable way to proceed?

[fredrik-bakke]

Since @VojtechStep has exams and this PR is crucial for our current refactoring efforts of synthetic homotopy theory, I'm thinking about merging this PR without the review comments being addressed. In that case I would address the review comments myself in #885. Would this be an acceptable way to proceed?

Sure, no problem! Alternatively, if you want to be more tidy about it you can push to his branch before merging it.

[VojtechStep]

I didn't get to it yesterday, but I should be able to address the comments this afternoon

[EgbertRijke]

Since @VojtechStep has exams and this PR is crucial for our current refactoring efforts of synthetic homotopy theory, I'm thinking about merging this PR without the review comments being addressed. In that case I would address the review comments myself in #885. Would this be an acceptable way to proceed?

Sure, no problem! Alternatively, if you want to be more tidy about it you can push to his branch before merging it.

I never figured out how it works to push into someone else's branch. I always get prompted with an error about permission to do so.

[EgbertRijke]

I didn't get to it yesterday, but I should be able to address the comments this afternoon

If you want to do it then I can wait, but I don't want to request changes from you during your exams.

(Note that I already resolved the merge conflict for you, so you will need to pull before making changes.)

[VojtechStep]

Alright, the comments should be addressed now