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

[Roman]

You can easily get the PHOAS representation of a regular Agda lambda
expression [1]. E.g.

    K : Term (⋆ ⇒ ⋆ ⇒ ⋆)
    K = ↓ const

    S : Term ((⋆ ⇒ ⋆ ⇒ ⋆) ⇒ (⋆ ⇒ ⋆) ⇒ ⋆ ⇒ ⋆)
    S = ↓ _ˢ_

Here `↓` takes an Agda combinator, specializes all type variables as
it desires and constructs the corresponding PHOAS term. The
implementation is just a matter of a few lines.

Constructing typed de Bruijn terms from metalanguage lambda terms is
much harder. When you do normalisation by evaluation, you use some
form of Kripke semantics in order to get an easy way to reify
target-language terms back. But PHOAS representation is basically a
shallow embedding of metalanguage terms which do not have the notions
of weakening, future contexts and such, so things become quite more
involved as witnessed by Adam Chlipala's elaborations Nils referred
to.

There is always a way to cheat, though. You can turn the PHOAS ->
untyped de Bruijn machinery into the PHOAS -> typed de Bruijn
machinery by checking that future contexts indeed extend past contexts
and throwing an error otherwise (which can't happed, because future
contexts always extend past contexts, but it's a metatheorem). Not a
type-theoretic way to do things, "but works". This is discussed in the
Andreas Abel's habilitation thesis [2] under the heading "Liftable
terms". I have an implementation of these ideas in Agda: [3]. Reifying
regular Agda lambda terms costs one postulate with this approach.

But I'm not a type theorist, so take it with a grain of salt.

[1] https://github.com/effectfully/random-stuff/blob/master/Normalization/PHOAS.agda
[2] http://www.cse.chalmers.se/~abela/habil.pdf
[3] https://github.com/effectfully/random-stuff/blob/master/Normalization/Liftable.agda