Zulip Chat Archive
Stream: triage
Topic: PR #4716: chore(category_theory/limits/preserves): preser...
Random Issue Bot (Nov 04 2020 at 14:15):
Today I chose PR 4716 for discussion!
chore(category_theory/limits/preserves): preserve limit of special shape
Created by @Bhavik Mehta (@b-mehta) on 2020-10-20
Labels: RFC, WIP
Is this PR still relevant? Any recent updates? Anyone making progress?
Johan Commelin (Nov 04 2020 at 14:30):
@Rob Lewis Can we configure the triage bot to choose PRs that are somewhat oldish?
Johan Commelin (Nov 04 2020 at 14:30):
This one is about two weeks old...
Bhavik Mehta (Nov 04 2020 at 15:05):
It's passively ongoing, I've taken out a part of it in #4857 and I'll cut up the original a bit more
Mario Carneiro (Nov 04 2020 at 15:27):
two weeks is the "oldish" cutoff
Johan Commelin (Nov 04 2020 at 15:32):
Hmm... can we move that to 1 month?
Johan Commelin (Nov 04 2020 at 15:32):
Actually, doesn't matter too much
Johan Commelin (Nov 04 2020 at 15:32):
Just "bad luck" that the bot chose something that's 2w+1d old
Rob Lewis (Nov 04 2020 at 16:05):
Two weeks seems old enough that a prod from the bot could have an affect. Makes more sense for some than others. But I think it' reasonable.
Bhavik Mehta (Nov 04 2020 at 16:16):
Could the bot use "last activity" rather than creation date? That PR had a push 4 days ago, so it feels odd to mark it as oldish
Rob Lewis (Nov 04 2020 at 16:19):
We could. The activity tracker is very sensitive. A bot updating a label counts as activity. It's basically a question of whether we prefer false positives or negatives.
Random Issue Bot (Jan 01 2021 at 14:29):
Today I chose PR 4716 for discussion!
chore(category_theory/limits/preserves): preserve limit of special shape
Created by @Bhavik Mehta (@b-mehta) on 2020-10-20
Labels: WIP
Is this PR still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Apr 14 2022 at 14:14):
Today I chose PR 4716 for discussion!
chore(category_theory/limits/preserves): preserve limit of special shape
Created by @Bhavik Mehta (@b-mehta) on 2020-10-20
Labels: WIP, merge-conflict
Is this PR still relevant? Any recent updates? Anyone making progress?
Bhavik Mehta (Apr 14 2022 at 16:26):
The title of this PR is pretty inaccurate now - most of the changes I already wanted from this are in mathlib, and what's left is the formalisation of some bits from a paper of Winskel. Essentially they allow you to show a functor preserves certain limits provided there are isomorphisms of the correct shape, but they don't need to be canonical. eg we have that a functor preserves binary products iff is_iso (prod_comparison G X Y) for all X Y, but it suffices for there to be any natural isos of the right shape, which may not be those (and in fact the isos given can be different to the "correct" ones). As far as I know, this result isn't particularly needed by anyone right now but I think it's pretty cool anyway. I'll update the descriptions.
Random Issue Bot (May 09 2022 at 14:20):
Today I chose PR 4716 for discussion!
chore(category_theory/limits/preserves): preserve limit of special shape
Created by @Bhavik Mehta (@b-mehta) on 2020-10-20
Labels: WIP, merge-conflict
Is this PR still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC