We explore the design of an intrinsically typed, tagless interpreter for stratified System F in Agda.