## 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) :=


Last updated: May 18 2021 at 22:15 UTC