Zulip Chat Archive

Stream: triage

Topic: issue #7051: Predicate for Kan extensions


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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