Something with universe levels

Stream: lean4

[Gabriel gomez]

  inductive Constant (a: Type) (x: Type) where
  | mk : a -> Constant a x

  inductive Choice (p q: Type -> Type) (x: Type) where
  | L : p x -> Choice p q x
  | R : q x -> Choice p q x

  def ValP i q x: Choice (Constant i) (q) x:= Choice.L (Constant i x)

the last line is failing with this:

cat.lean:38:55
application type mismatch
Choice.L (Constant i x)
argument
Constant i x
has type
Type : Type 1
but is expected to have type
Constant i x : Type

maybe someone know why this is failing?

[Gabriel gomez]

I Found the error, sometimes I confused the diferent levels and go the wrong way.

[Marcus Rossel]

At the end of your last line you want to be using Constant.mk.