[Merged by Bors] - feat: change Type to Sort in Algebra/Classes, fix some priorities
#10354
Conversation
sgouezel
added
the
awaiting-review
| @@ -67,219 +67,219 @@ set_option autoImplicit true | |||
| universe u v | |||
|
|
|||
| -- porting note: removed `outParam` | |||
| class IsSymmOp (α : Type u) (β : Type v) (op : α → α → β) : Prop where | |||
| class IsSymmOp (α : Sort u) (β : Sort v) (op : α → α → β) : Prop where | |||
There was a problem hiding this comment.
Can you please record a summary (maybe as library note?) that motivates why these classes should be defined on Sorts instead of Types?
It's not clear to me why we would want to allow Props here...
There was a problem hiding this comment.
One thing I had to fix in #10335 was that the IsTrans defined in this file gained higher priority, and then Lean tried to apply it to Eq in calc blocks and failed because of universe issues, as IsTrans was only defined on Type u and it was trying to apply it to Prop. One fix was to extend the IsTrans to Sort instead of Type, and then I thought that it would make sense to have all these definitions on Sort as it makes universe unification a bit easier, for essentially no cost. A better fix, IMHO, would be to just remove this file as we don't really use it.
There was a problem hiding this comment.
We can also discard the PR, it's not as if it's really important.
There was a problem hiding this comment.
I think your motivation is valid. Let's just merge this.
bors merge
jcommelin
added
awaiting-author
sgouezel
added
awaiting-review
|
Build failed (retrying...): |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Algebra/Classes, fix some prioritiesAlgebra/Classes, fix some priorities
sgouezel
added
ready-to-merge
These changes were needed to fix the build in the (unsatisfactory) experiment #10335. They seem useful to have in any case, as independent refactors could stumble on the same issues.