Zulip Chat Archive

Stream: triage

Topic: issue #2725: `push_hom` and `pull_hom` tactics


Random Issue Bot (Feb 14 2021 at 14:19):

Today I chose issue 2725 for discussion!

push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: feature-request, help wanted, meta

Is this issue still relevant? Any recent updates? Anyone making progress?

Scott Morrison (Feb 14 2021 at 22:47):

I haven't thought about this in a while. But I'd certainly like to have something like this.

Scott Morrison (Feb 14 2021 at 22:48):

Indeed, in category theory proofs I can think of lots of related tools: push/pull for _functor, _eq_to_hom, ... I think all of them would just be named simp sets, and possibly rather light wrappers around them.

Eric Wieser (Feb 15 2021 at 05:30):

Is there a mechanism to say "use this simp set with every lemma reversed"?

Johan Commelin (Feb 15 2021 at 06:09):

On the other hand, since mathlib moved to bundled functions, I've had a lot less need for this type of tactics, because simp is now just a lot better at this.

Yury G. Kudryashov (Feb 15 2021 at 18:58):

simp is good as push_hom but sometimes (not often) I want pull_hom.

Random Issue Bot (Mar 17 2021 at 14:26):

Today I chose issue 2725 for discussion!

push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: feature-request, help wanted, meta

Is this issue still relevant? Any recent updates? Anyone making progress?

Random Issue Bot (Dec 07 2021 at 14:21):

Today I chose issue 2725 for discussion!

push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help wanted, meta, feature-request

Is this issue still relevant? Any recent updates? Anyone making progress?

Anne Baanen (Dec 07 2021 at 15:39):

With #9888, the set of lemmas that have to be reversed should at least be smaller :)

Random Issue Bot (Jan 05 2022 at 14:15):

Today I chose issue 2725 for discussion!

push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help wanted, meta, feature-request

Is this issue still relevant? Any recent updates? Anyone making progress?

Random Issue Bot (Jan 17 2022 at 14:18):

Today I chose issue 2725 for discussion!

push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help wanted, meta, feature-request

Is this issue still relevant? Any recent updates? Anyone making progress?

Random Issue Bot (May 02 2022 at 14:20):

Today I chose issue 2725 for discussion!

push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help wanted, meta, feature-request

Is this issue still relevant? Any recent updates? Anyone making progress?

Random Issue Bot (May 27 2023 at 14:07):

Today I chose issue 2725 for discussion!

push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help-wanted, t-meta, feature-request

Is this issue still relevant? Any recent updates? Anyone making progress?

Random Issue Bot (Jul 23 2023 at 14:07):

Today I chose issue 2725 for discussion!

push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help-wanted, t-meta, feature-request

Is this issue still relevant? Any recent updates? Anyone making progress?

Random Issue Bot (Jul 31 2023 at 14:07):

Today I chose issue 2725 for discussion!

push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help-wanted, t-meta, feature-request

Is this issue still relevant? Any recent updates? Anyone making progress?


Last updated: Dec 20 2023 at 11:08 UTC