We provide an intrinsically-typed mechanization of System Rω with a shallow embedding / denotation into Agda. A suitable reviewer should have some experience with Agda, the Agda standard library, and language mechanization. The mechanization is a shallow embedding, so the metatheory follows from a total denotation. This means the artifact has very few of the lemmas, theorems, and infrastructure one might find in the mechanization of an operational semantics. However, by nature of embedding into a predicative system, our ASTs and denotational functions are burdened fairly heavily by level stratification. More experience with Agda over strict mechanization is thus welcome.