whisper Current status $ racket main.rkt type of term: let id : (A : 𝕌) → (_ : A) → A = λA.λx.x; id 𝕌 is (_ : 𝕌) → 𝕌