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