Zulip Chat Archive

Stream: new members

Topic: elaborator bug


view this post on Zulip Kenny Lau (Feb 08 2019 at 01:38):

import category_theory.category data.quot

universes v u

namespace category_theory

variables (C : Type u) [category.{v} C]

structure initial_object :=
(carrier : C)
(of_carrier : Π x, carrier  x)
(eq_of_carrier :  x,  f : carrier  x, f = of_carrier x)

end category_theory

view this post on Zulip Kenny Lau (Feb 08 2019 at 01:38):

error: invalid reference to undefined universe level parameter 'v'

view this post on Zulip Reid Barton (Feb 08 2019 at 02:56):

@Kenny Lau Yeah, this is the usual known elaborator bug which means you need to instead write

variables {C : Type u} [𝒞 : category.{v} C]
include 𝒞

view this post on Zulip Scott Morrison (Feb 08 2019 at 04:05):

Is it really a bug? I thought it was an intentional decision to not make use of variables if doing so required fixing an otherwise unspecified universe.

view this post on Zulip Scott Morrison (Feb 08 2019 at 04:07):

@Sam Jessup, I've made a new "topic" for your question --- you're more likely to get useful answers if you keep different conversations separate.

view this post on Zulip Reid Barton (Feb 08 2019 at 04:07):

If that was the issue you'd get a different error

view this post on Zulip Scott Morrison (Feb 08 2019 at 04:07):

You should ask Kenny Lau to tell you what he's already done from Atiyah-MacDonald; there might be some significant overlap.

view this post on Zulip Scott Morrison (Feb 08 2019 at 04:08):

I'm confused. What is the bug?

view this post on Zulip Reid Barton (Feb 08 2019 at 04:11):

The bug is that the elaborator produces an expression referring to v without including v among the universe parameters of the declaration

view this post on Zulip Scott Morrison (Feb 08 2019 at 04:12):

Oh! I see. I had never understood this issue properly.

view this post on Zulip Reid Barton (Feb 08 2019 at 04:13):

similar I think to https://github.com/leanprover/lean/issues/395, but evidently different


Last updated: May 11 2021 at 00:31 UTC