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

[Nils Anders Danielsson]

On 2018-02-27 14:26, Philip Wadler wrote:
> The typed DeBruijn representation is well known, as are typed PHOAS
> and untyped DeBruijn.  It is easy to convert PHOAS to untyped
> DeBruijn.  Is it known how to convert PHOAS to typed DeBruijn?

I haven't checked the details, but Adam Chlipala seems to discuss this topic:

   http://adam.chlipala.net/cpdt/html/Intensional.html

-- 
/NAD