An Agda formalization of the halting problem for Turing machines