Refactor precomposition #937
Conversation
|
This is certainly a nice improvement to the library, but I worry that the combination of refactoring precomposition and removing unused imports is going to lead to a lot of merge conflicts for other PRs. Therefore I wonder if it is best to hold off on merging this PR until we have gotten more of the other PRs in the pipeline merged. |
I merged all the PRs that were marked as ready that were opened prior to this one, and a few more. So now I think we shouldn't hold off on merging this one anymore. |
|
If you think it’s done please use that merge button:) I need to train you guys to use it more 😄 |
|
And thank you for the review btw! You definitely caught some things that needed fixing! |
|
My pleasure! |
This PR refactors precomposition, following difficulties that people have been facing around where to put stuff involving precomposition, and cyclic dependencies that are too easily arising. In fact, it was quite a knot to untie. At the core of the knot was what is now called the (dependent) universal property of equivalences, which is in its own separate file now. I created tables, and did some minor code formatting, but please note that this is not the main purpose of this PR.
This PR refactors precomposition, following difficulties that people have been facing around where to put stuff involving precomposition, and cyclic dependencies that are too easily arising. In fact, it was quite a knot to untie. At the core of the knot was what is now called the (dependent) universal property of equivalences, which is in its own separate file now. I created tables, and did some minor code formatting, but please note that this is not the main purpose of this PR.
This PR refactors precomposition, following difficulties that people have been facing around where to put stuff involving precomposition, and cyclic dependencies that are too easily arising. In fact, it was quite a knot to untie. At the core of the knot was what is now called the (dependent) universal property of equivalences, which is in its own separate file now. I created tables, and did some minor code formatting, but please note that this is not the main purpose of this PR.