Can type information be encoded in the untyped lambda calculus?

I'm going to take the few pieces of knowledge I have about lambda calculi and ask a pair of very uninformed questions :-)

Is it possible to "embed" the corners of the lambda cube within the untyped lambda calculus?

It would seem that this might lead to a language where the programmer implements the type system in the language, rather than having it already implemented in the compiler. Also, maybe the concept of type system could be generalized to "any arbitrary compile-time or run-time constraint checking". Does such a language already exist?

As mentioned in the comments, it is possible to reduce simply typed lambda calculus to untyped lambda calculus. This is the approach associated with Alonzo Church, called "Church Types" or "intrinsic types". Here, types are embedded in the language, and are intrinsic to the language. Still, the language can be stripped of it's types.

However, it is also possible to construct simply typed lambda calculus from untyped lambda calculus. This approach is associated with Haskell Curry, called "Curry Types" or "extrinsic types". Here, types can be derived from the AST of the language.

The latter type is what you are looking for. A thorough overview of the subject is here

StackExchange Computer Science Q#19767, answer score: 4