Indiscrete precategories #896
Conversation
Co-authored-by: Egbert Rijke <[email protected]>
This is an experimental attempt to get some sort of uniform treatment of iterated type families going. Work in progress, and ideas are very welcome. --------- Co-authored-by: Fredrik Bakke <[email protected]>
|
Would it be possible to rebase this one, so that I can see what actually changed? Because while it had the appearance that I "just merged" the other to PRs today, I did actually look over them quickly. But these 9000 lines are too much. |
|
Done |
|
Or, at least, GitHub is telling me there are only 851 lines of additions now |
|
Great, thanks! |
There was a problem hiding this comment.
Very nice pull request! My apologies for letting this linger for so long... I am again reviewing this from the gas station with free wifi:P
I made some suggestions for additional files that I think would be nice to have. Feel free to defer these suggestions to future work. It would be also be good to merge this pull request without the additional files.
|
|
||
| initial-functor-Precategory : functor-Precategory initial-Precategory C | ||
| pr1 initial-functor-Precategory () | ||
| pr1 (pr2 initial-functor-Precategory) {()} |
There was a problem hiding this comment.
Lol, I haven't seen that one before;)
There was a problem hiding this comment.
Is there something here you would want me to change?
|
Apparently you didn't get to updating the PR yet, but I'm going to merge it. We can resolve the review suggestions in a next PR. |
This is a small(er) one. It
Depends on #886 and #880.