elaborator bug

Stream: new members

[Kenny Lau]

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

[Kenny Lau]

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

[Reid Barton]

@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 𝒞

[Scott Morrison]

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.

[Scott Morrison]

@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.

[Reid Barton]

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

[Scott Morrison]

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

[Scott Morrison]

I'm confused. What is the bug?

[Reid Barton]

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

[Scott Morrison]

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

[Reid Barton]

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