feat(category_theory): assorted small changes from the old limits PR #512
Conversation
semorrison
force-pushed
the
category-theory-assorted
branch
from
cf5b437
to
2af9d94
Compare
|
|
||
| def discrete (α : Type u₁) := α | ||
|
|
||
| @[extensionality] lemma plift.ext {P : Prop} (a b : plift P) : a = b := |
There was a problem hiding this comment.
"Orphaning" an extensionality lemma like this is a bad idea. It means the behavior of ext will change depending on whether this module category_theory.discrete_category is imported, and especially since imports are transitive in Lean, this is something one has little control over.
The best place to put this would be either together with the definition of plift (impossible in this case), or with the definition of ext, or in some module which we can assume is "always" imported--I believe logic.basic qualifies. Also possible is to define the lemma here and give it the extensionality attribute locally.
However, I don't really understand why we are writing extensionality lemmas for subsingletons. Isn't this something we can solve once and for all by marking subsingleton.elim with extensionality? Or by modifying ext to try applying it?
There was a problem hiding this comment.
I've moved this next to ulift.ext in tactics/ext.lean.
ext doesn't want to use subsingleton.elim for now. I agree this would be a good addition, but I think requires modifying ext.
There was a problem hiding this comment.
Just pinging @cipher1024 in case he knows readily how hard this would be.
semorrison
force-pushed
the
category-theory-assorted
branch
from
9da1aa8
to
829fdb0
Compare
|
Hooray! |
This consists of the remaining changes from the old limits PR, not including anything to do with special shapes.
Most of it is minor, with the exception of introducing discrete categories.
(I've also rebased what remains of my "special shapes" limits work onto this commit.)