A simple way to show Turing-completeness of a particular language is by encoding a Turing-equivalent computation system in it. Here we show Turing-completness of Agda, by encoding the Cyclic Tag System in it.
The Boolean Blindness blog post by Dr. Robert Harper presents a generally excellent point: the use of Booleans is inherently connected with a loss of information, the so-called Boolean Blindness.
For example, even if we for some list
xs know that the expression
all even xs = True holds, we often can not use that information further along in our program1 and we still have to handle the cases where an element is odd, even though such case is impossible in practice.