Universe levels issues

Stream: general

[shiki]

Hi, there. I got stuck writing one little definition.

inductive t : {A B:Type} -> A -> B -> Type
-- | mkr {T:Type}{v:T}: @t T T v v
| mkp :
  (f:A -> B) -> (h:B -> A) ->
  -- ((a:A) -> (b:B) -> (t (f a) b) × t a (h b)) ->
  t A B

Commented sections are the places of trouble. Lean says there's some issue with universe levels or something, I am not quite sure. Can it be made to work?

[Marcus Rossel]

Here's mkr working:

inductive t : {A B : Type} → A → B → Type _
  | mkr {T : Type} {v : T} : @t T T v v
  | mkp : (f : A → B) → (h : B → A) → t A B

I changed the type of t from Type (aka Type 0) to Type _, which tells Lean to figure out what the universe level should be. Writing #check t shows that Type 1 is necessary.

[shiki]

Marcus Rossel said:

Here's mkr working:

inductive t : {A B : Type} → A → B → Type _
  | mkr {T : Type} {v : T} : @t T T v v
  | mkp : (f : A → B) → (h : B → A) → t A B

I changed the type of t from Type (aka Type 0) to Type _, which tells Lean to figure out what the universe level should be. Writing #check t shows that Type 1 is necessary.

Oh, I didnt know that. But Id like to get this working

inductive t : {A B : Type} → A → B → Type _
  | mkr {T : Type} {v : T} : @t T T v v
  | mkp :
    (f : A → B) → (h : B → A) →
    ((a:A) -> (b:B) -> (t (f a) b) × (t a (h b))) ->
    @t A B a b

Lean tells me
(kernel) invalid nested inductive datatype 'Prod', nested inductive datatypes parameters cannot contain local variables.

What does this error mean?

[Jovan Gerbscheid]

It looks to me like the variables a and b in @t A B a b aren't introduced anywhere. Maybe you got the brackets wrong?