get_limit_cone

Stream: maths

[Scott Morrison]

Hi @Markus Himmel (and any other category theorists here at the moment!)

I'm running into some annoying problems with get_limit_cone --- just that there isn't a good simp normal form set up at the moment. I'm seeing things like (get_limit_cone F).cone.X appearing, which of course is definitionally equal to just limit X.

Options:

1. I add the simp lemmas that reduce projections of get_limit_cone to the "canonical" ways of summoning these objects.
2. I just remove the limit_cone structure entirely, in favour of a sigma type.

Any preferences?

[Markus Himmel]

Personally, I imagined that the library would slowly migrate from having parameters like {c : cone F} (hc : is_limit F) to (c : limit_cone F), so I'm in favor of having something called limit_cone. I'm not 100% sure how your sigma type idea would look.

[Scott Morrison]

Sounds good. I will add some simp lemmas as I need them.

[Reid Barton]

I wonder whether this will result in too many ways to say the same thing? You can't really get rid of is_limit since it's needed for most theorems where it appears in the conclusion. Of course for hypotheses this can't cause too much trouble, since you can always write \<c, hc\> where you would write hc before (or c could even be implicit in the limit_cone structure), though Lean's automation might find this slightly challenging.

[Reid Barton]

I'd guess that more than half the time when you know something is a limit, it's not because you got it from limit or from a hypothesis, but rather you had the cone already and then checked it was a limit, either directly, or using some theorem about a functor preserving/reflecting limits, or by pasting pullback squares, etc.

[Scott Morrison]

It turned out once I got myself straightened out this issue wasn't actually a problem for me today, so I haven't fixed it either way!