Add a (work in progress) package on model categories / weak factorization systems

[DenSinH]

This is still a bit of a work in progress. I am also not 100% sure it will compile yet in UniMath. Suggestions are welcome of course.

There is one lemma (and one lemma that depends on it) that depends on the axiom of choice, which has been admitted in the proof now, but this of course needs some work in the future.

I don't know why it also included the commits from my other PR...

[benediktahrens]

Thanks a lot for filing this PR. I have made a few small comments.

Can you describe what the issue is with the admitted proof? You could add the axiom of choice as a hypothesis. Possibly we also have a suitable statement of AC in Foundations?

[Kfwullaert]

A general question: You have defined the arrow category, however, the definition of morphismclass does not make use of this. Why did you not define morphismclass as a subtype of the type of objects in the arrow category?

[DenSinH]

A general question: You have defined the arrow category, however, the definition of morphismclass does not make use of this. Why did you not define morphismclass as a subtype of the type of objects in the arrow category?

This is something that I potentially wanted to change, it seems fitting here, but changing "normal morphisms in a category C" to "objects of arrow C" in some proofs mainly in WFS.v messed up a lot of things, but I am not sure why. Though in the case of the definition of a morphism class, I don't think I will run into problems, and I should and will definitely change it.

[DenSinH]

Thanks a lot for filing this PR. I have made a few small comments.

Can you describe what the issue is with the admitted proof? You could add the axiom of choice as a hypothesis. Possibly we also have a suitable statement of AC in Foundations?

True yes, but possibly it might be better to change some other definitions so that we have the actual lifting data in a WFS, so that the axiom of choice is no longer an issue. I am already working further on an article by Garner, where he defines cofibrantly generated WNFSs. In this situation, the axiom of choice is no longer an issue, since we actually have the lifting data available. I guess I should still change it to pass the axiom of choice as a parameter, but the theorem itself might change, I am not sure yet...

[Kfwullaert]

Thanks a lot for filing this PR. I have made a few small comments. Can you describe what the issue is with the admitted proof? You could add the axiom of choice as a hypothesis. Possibly we also have a suitable statement of AC in Foundations?

True yes, but possibly it might be better to change some other definitions so that we have the actual lifting data in a WFS, so that the axiom of choice is no longer an issue. I am already working further on an article by Garner, where he defines cofibrantly generated WNFSs. In this situation, the axiom of choice is no longer an issue, since we actually have the lifting data available. I guess I should still change it to pass the axiom of choice as a parameter, but the theorem itself might change, I am not sure yet...

If the lifting is data, don't you have an issue with the morphism classes? Since fibrations are completely determined by the acyclic cofibrations in the sense that the fibrations as those morphisms with the right lifting property against the acyclic cofibrations. If you define lifting as a data, then you can no longer define the fibrations in this way because being a fibration is no longer a property.

[DenSinH]

Thanks a lot for filing this PR. I have made a few small comments. Can you describe what the issue is with the admitted proof? You could add the axiom of choice as a hypothesis. Possibly we also have a suitable statement of AC in Foundations?

True yes, but possibly it might be better to change some other definitions so that we have the actual lifting data in a WFS, so that the axiom of choice is no longer an issue. I am already working further on an article by Garner, where he defines cofibrantly generated WNFSs. In this situation, the axiom of choice is no longer an issue, since we actually have the lifting data available. I guess I should still change it to pass the axiom of choice as a parameter, but the theorem itself might change, I am not sure yet...

If the lifting is data, don't you have an issue with the morphism classes? Since fibrations are completely determined by the acyclic cofibrations in the sense that the fibrations as those morphisms with the right lifting property against the acyclic cofibrations. If you define lifting as a data, then you can no longer define the fibrations in this way because being a fibration is no longer a property.

Yes, this was the main issue with defining it this way, the definition of morphism class would not suffice to do this. I guess perhaps a way to circumvent using the axiom of choice would be to pass a function that maps morphisms to their lifting data. I mainly just tried to keep the axiom of choice out of it.

[benediktahrens]

@DenSinH : do you have any questions about the suggestions made to this PR? Is anything unclear?

[DenSinH]

@DenSinH : do you have any questions about the suggestions made to this PR? Is anything unclear?

Nope! Sorry just forgot to make the changes, I'll add them tomorrow!

[DenSinH]

I'm not sure how to fix this issue with the clashing notations...