Help fixing universes for an inductive definition

Stream: general

[Tej Chajed]

I have a lot of experience with Coq but am just getting started with Lean. I'm trying to write down an inductive type in Lean but can't get the universes to work out. I couldn't find much documentation on universes in Lean so I'm not sure what I can do about this. The analogous type works out in Coq without any universe parameters or annotations.

universes u v w.

def stream (a: Type u) : Type u := nat → a.

inductive ckt : Type u → Type u → Type (u + 1)
| delay {a: Type u} : ckt (stream a) (stream a)
| lifting {a b: Type u} (f: a → b) : ckt (stream a) (stream b)
| seq {a b c: Type u} (f1: ckt a b) (f2: ckt b c) : ckt a c
| feedback {a: Type u} : ckt unit a

Concretely I get an error that in the feedback constructor term unit has type Type : Type 1 but was expected to have type Type u : Type (u+1). I also wasn't able to use ckt.{u} to provide an explicit universe, because it's fixed by the universe variable I guess.

[Mario Carneiro]

try punit instead of unit

[Mario Carneiro]

your last constructor is weird since it gives 3 arguments to ckt

[Tej Chajed]

(fixed the unrelated issue with passing three arguments to ckt, thanks for pointing that out)

[Tej Chajed]

oh interesting that does work! punit is just universe polymorphic unit I guess?

[Kevin Buzzard]

Yes. Unlike Coq, Lean does not have cumulative universes.