[Coq-Club] [Agda] Defining Coq(w/o Prop) in Agda using Induction Recursion

[Nils Anders Danielsson]

On 2013-12-03 02:06, Edwin Westbrook wrote:
> Thus, it seems like this is not really an encoding of all of Coq into
> the first level of Agda.
>
> Do I have this right? Or am I missing something?

That's right.

-- 
/NAD