Zulip Chat Archive
Stream: triage
Topic: issue #7051: Predicate for Kan extensions
Random Issue Bot (Apr 16 2021 at 14:23):
Today I chose issue 7051 for discussion!
Predicate for Kan extensions
Created by @Bhavik Mehta (@b-mehta) on 2021-04-06
Labels: feature-request, medium
Is this issue still relevant? Any recent updates? Anyone making progress?
Bhavik Mehta (Apr 16 2021 at 14:24):
No recent updates as far as I know, it's a feature a couple of people agree would be nice but there seems to be no need for it yet
Adam Topaz (Apr 16 2021 at 15:48):
I actually thought about this (very briefly!). It seems the one natural way to phrase this would be to say that certain limit cones exist, but eventually you're forced to write down something like "this is a limit cone for a functor F whose cone point is this object X". Do we have some idiomatic way to say that something is a cone with a specified cone point?
Adam Topaz (Apr 16 2021 at 15:49):
I mean, this is "just" a morphism from the constant functor with value X to the given functor F, but is this the best way to write it down?
Scott Morrison (Apr 17 2021 at 11:24):
Right at the beginning of cones.lean is:
/--
Functorially associated to each functor `J ⥤ C`, we have the `C`-presheaf consisting of
cones with a given cone point.
-/
@[simps] def cones : (J ⥤ C) ⥤ (Cᵒᵖ ⥤ Type v) :=
Random Issue Bot (Oct 19 2021 at 14:19):
Today I chose issue 7051 for discussion!
Predicate for Kan extensions
Created by @Bhavik Mehta (@b-mehta) on 2021-04-06
Labels: medium, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Nov 05 2021 at 14:19):
Today I chose issue 7051 for discussion!
Predicate for Kan extensions
Created by @Bhavik Mehta (@b-mehta) on 2021-04-06
Labels: medium, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Feb 02 2022 at 14:16):
Today I chose issue 7051 for discussion!
Predicate for Kan extensions
Created by @Bhavik Mehta (@b-mehta) on 2021-04-06
Labels: medium, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jun 30 2023 at 14:07):
Today I chose issue 7051 for discussion!
Predicate for Kan extensions
Created by @Bhavik Mehta (@b-mehta) on 2021-04-06
Labels: medium, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Jun 30 2023 at 21:16):
Heh, this came up today in Copenhagen!
Last updated: Dec 20 2023 at 11:08 UTC