Bump stdlib to 2.0 #406
Bump stdlib to 2.0 #406
Conversation
Didn't notice that I'd ended up in Functor.Instance in the previous commit
I couldn't get the proofs working with Surjective yesterday so I used SplitSurjective instead but that turned out to be too strict later
…tching constructor
… function hierarchy
…ion hierarchy and updated Preorder
|
Status: I've been working through the modules in alphabetical order. I've skipped |
…es to two proofs.
|
Wow, @JacquesCarette, you've stormed through that! |
|
I ended up spending close to 12 hours yesterday single-mindedly pushing through this. I'd definitely appreciate a review @Taneb . I know there's quite a few things to clean up, but that's so much easier than the first pass. |
There was a problem hiding this comment.
I've had a quick look through and highlighted (all minor) problems I've seen.
Can I ask you to take a close look at Categories.Functor.Properties, @JacquesCarette ? It probably has the most substantial changes
src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda
Outdated
Show resolved
Hide resolved
|
(I'm going to use the review facility to leave additional notes for myself) |
…tions of CT more closely.
Closes #405. Supercedes #352.
I ran into difficulty trying to make
Categories.Yonedawork with the new function hierarchy so I'm opening this as a draft.Many of the changes could be made tidier.
Difficulties encountered so far:
Categories.Category.Instance.SetoidsandCategories.Adjoint.Matecould both do with a definition of equality of functions between setoids. I've inlined it for the former but didn't for the latter, because we just want the relation and it'd be too much of a mess to define it there locally too.Categories.Yonedathat I bounced off it. I may give this another go at some point.Other maintainers of the library are explicitly invited to contribute to this PR.