Proving Turing Completeness by creating a compiler to a Turing Complete language
No. It's usually relatively easy to compile a language (Turing complete or otherwise). At a very simplistic level, a compiler flattens an abstract syntax tree into a list of instructions. This can usually be done by a simple structural induction over the syntax tree. Optimization passes often do data flow or control flow analyses that would be harder to represent as a simple structural induction.

You can make a practical demonstration by programming a compiler for the untyped lambda calculus into some simple Turing complete stack-based machine in Agda or some other non-Turing complete language.

However, just as an extreme example, the "compiler" could be the identity function. If you meant that you could write a compiler for any Turing complete language, then that wouldn't be possible simply because the semantics of the language may require executing arbitrary code (e.g. Common Lisp macros) to elaborate the syntax or otherwise to produce a correct compiler.