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

[Edwin Westbrook]

(Sorry to be a little late on this thread…)

This is a very interesting link, thanks!

One question: it looks like these are predicative universes, and that this encoding does not really handle Coq’s impredicative sort Prop. Quoting Conor:

"This is rather unlike Coq, where there is one impredicative universe of propositions living at the base of the hierarchy, but allowing quantification over higher levels. Here, every layer of sets has its own distinguished fragment of props."

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?

Thanks,
-Eddy

On Nov 26, 2013, at 1:55 AM, Nils Anders Danielsson <nad at cse.gu.se> wrote:

> On 2013-11-26 00:38, Abhishek Anand wrote:
>> Has someone tried to define(using IR) a universe closed under both PI
>> and strictly-positive-Inductive type-constructors? (Coq's first
>> universe seems to match that description precisely.)
> 
> Yes:
> 
>  Hier Soir, an OTT Hierarchy
>  Conor McBride
>  http://sneezy.cs.nott.ac.uk/epilogue/?p=1098
> 
>> If so, does the definition fit in Set 0 of Agda?
> 
> Yes: "We’ve built something like Coq’s hierarchy inside Agda’s lowest
> level."
> 
> -- 
> /NAD
>