got round to installing emacs and agda on the current laptop and writing pointedly naive versions of an STLC typechecker with elaboration to an intrinsically typed version and typed-from-the-well interpreter to follow when I get round to it