On the one hand, you can think of starting with some given notion of computation (the lambda-calculus, say, or x86 machine code), and then you can think of types as picking out particular subsets of the set of valid programs. (In jargon, this is "types as retracts".)
In this view, a type is a property of a program. On the one hand, you can say that only things which pass type-checking are programs, and things which don't type check are simply not well-formed programs. In this view, a type is a kind of grammaticality constraint.
If you don't have a model of the untyped lambda calculus, you can't speak formally about the first view, which is very limiting. This is because being able to shift between the views is important for thinking flexibly about different kinds of problems.
Of course, you can also try to combine these two views. A few years back, Noam Zeilberger and Paul-Andre Mellies wrote a gorgeous paper, "Functors are Type Refinement Systems", which lays out the principles of how these two views interact.
LC is clearly "untyped" in that it doesn't carry any type system, but that's a distinct idea from "dynamically typed introspection". That's an engineering system.
So maybe my error is to read into "dynamic types" as something more than the most utilitarian reading, but I also think that's usually what the "debate" ends up being about.
Also, type theory is a mathematical/logical theory first, the connection to programming languages was discovered long after it was developed.
Short of it is that I'm reading "dynamic typing" as the engineering discipline involved in building systems that introspect that sum in meaningful ways.