[Merged by Bors] - feat: port CategoryTheory.Comma #2260
Conversation
joelriou
commented
Feb 13, 2023
joelriou
commented
joelriou
added
awaiting-review
Mathlib/CategoryTheory/Comma.lean
Outdated
| left : A --:= by obviously | ||
| right : B --:= by obviously |
There was a problem hiding this comment.
Can you use by aesop_cat here? That is now typically used as replacement for obviously/tidy.
There was a problem hiding this comment.
I know, but I am not sure what by aesop_cat would do here because left/right are data, not Prop fields. Would it have any effect at all?!
There was a problem hiding this comment.
Surprising that there was . obviously there in the first place. I think Scott got a bit carried away. I would suggest just deleting these comments, and leaving a porting note (that the Lean 3 version did not really make sense in the first place). Also in CommaMorphism below, except for the equational field w.
There was a problem hiding this comment.
I have just PRed this leanprover-community/mathlib#18440
There was a problem hiding this comment.
Actually, it turns out that these by obviously were necessary in mathlib3. The test mathlib PR just above does not compile. The reason is that for (co)structured_arrow, morphisms between initial/terminal objects could be filled automatically by obviously. Then, I have added by aesop_cat in this mathlib4 PR, and we may hope for the best that when we have limits in mathlib4, aesop_cat will be able to fill the obvious fields in (co)structured_arrow .
There was a problem hiding this comment.
I would just add explicit terms wherever needed in mathlib 3; they can't be too complicated right?
There was a problem hiding this comment.
These terms are easy. Doing so more or less forces the user to use the explicit constructors like structured_arrow.mk and structured_arrow.hom_mk (rather than providing the relevant fields and relying on automation for the rest). This should eventually make the code cleaner, and easier to maintain/port.
semorrison
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded:
|
bors
bot
changed the title
