id : (l : Level) -> (a : Set l) -> (x : a) -> a
id = \(l : Level) -> \(a : Set l) -> \(x : a) -> x

unitfoo : (_ : One) -> One
unitfoo = \(Unit : One) -> Unit

-- W-types: https://cs.stackexchange.com/a/55674/45548
-- for any n : Level, B : Set ? and any A : B -> Set ?, the following is allowed:
-- data[W] T : Set n where
--   c : (x : B) -> (_ : A x -> T) -> T

-- TODO: how parametric can n/n1/n2 be?

-- data Nat : Set 0 where
--   zero : Nat
--   succ : Nat -> Nat
-- ~>
-- B = One + One
-- A (inj1 Unit) = Void
-- A (inj2 Unit) = One
-- data[W] Nat : Set 0 where
--   c : (x : B) -> (_ : A x -> Nat) -> Nat

-- data List (C : Set 0) : Set 0 where
--   nil : List C
--   cons : C -> List C -> List C
-- ~>
-- B = 
-- data[W] List (C : Set 0) : Set 0 where
--   c : 

-- data Vec (A : Set 0) : Nat ->