## Stream: new members

### Topic: elaborator bug

#### 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


#### Kenny Lau (Feb 08 2019 at 01:38):

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

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


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

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

#### Reid Barton (Feb 08 2019 at 04:07):

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

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

#### Scott Morrison (Feb 08 2019 at 04:08):

I'm confused. What is the bug?

#### 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

#### Scott Morrison (Feb 08 2019 at 04:12):

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

#### 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