whisper This project tests ability of typed/racket by implementing conversion checking algorithm, you can run racket main.rkt to get the following result. type of term: let id : (A : 𝕌) → A → A = λA.λx.x; id 𝕌 is 𝕌 → 𝕌