Can one get Turing-completeness without nontermination?
Many total languages, including Agda and Coq, allow you to define coinductive data types. These model infinite objects, like infinite lists.

Obviously, a function producing an infinite list cannot terminate. However, it must, in a total language, be productive. This means that any finite prefix of the produced infinite list can be computed in finite time. Coq and Agda have productivity checkers to ensure this, like they have termination checkers for functions which consume inductive data types.

Using these coinductive data types, you can model infinite executions. In the example you linked, 'running' a brainfuck program produces a trace, which is a potentially-infinite list of machine states.

Whether this is enough to declare the language 'Turing-complete' is, I guess, a question for philosophers. Agda only ever allows you to inspect a finite prefix of the generated trace, so you can't 'run' a program for an infinite amount of time. Then again, no physical machine can run a program for an infinite amount of time. And in practice, you can just disable Agda's termination checker for the one function that prints out your potentially-infinite trace.