[Agda] Typed DeBruijn, typed Phoas, and untyped DeBruijn

[Roman]

Agda doesn't have a built-in deriving machinery, but Agda has tactics
which can be used to implement it. Ulf's `agda-prelude` allows to
derive decidable equality [1]. The downside is that `agda-prelude` is
not compatible with the standard library. There are several instances
you can derive with this library, but there is no strongly typed
representation of data types, hence if you want to derive your own
instances, you'll need to roll out substitution, unification, de
Bruijn indices/levels shifting and other tools from scratch and deal
with weakly typed `Term`s which is inconvenient and error-prone.

I have a library [2] that is compatible with the standard one and
allows to derive decidable equality and has a typed data type
representation (based on The Gentle Art of Levitation) and even though
it's able to handle a vast amount of data types (universe
polymorphism, implicit and instance arguments, indices and parameters,
higher-order induction -- all of these are supported), there are
practical (you can't reflect mutually recursive data types) and
theoretical limitations (you can't reflect non-strictly-positive,
inductive-inductive data types and most notably there is no internal
notion of polarity like in the Indexed Functors approach [4]).
Deriving your own instances is complicated and requires knowledge of
internals of the library. Still inconvenient, but not as error-prone
as dealing with weakly typed `Term`s.

I'd say switch to `agda-prelude` and use it.

[1] https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda
[2] https://github.com/effectfully/Generic
[3] https://pages.lip6.fr/Pierre-Evariste.Dagand/papers/levitation.pdf
[4] https://www.andres-loeh.de/IndexedFunctors/