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

[Abhishek Anand]

(because of the relevance of this question to both Coq and Agda
communities, I'm posting it to both lists.)

Hi,
I've been curious about the usefulness of induction recursion(IR)
in defining universes. The canonical use-case of Induction-Recursion
seems to be in defining a universe closed under dependent functions(PI).
One cool thing about the Inductive-Recursive formulation of such a universe
is that it fits in Set 0
(the first universe of Agda(or any similar methatheory supporting IR)).

Converting this definition to an Inductive one makes its type jump to Set 1
(This was discussed in
http://comments.gmane.org/gmane.science.mathematics.logic.coq.club/11380.
 see Andrew Cave's comment)

(When I mention Coq below, I really mean Coq without Prop.)

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.)
If so, does the definition fit in Set 0 of Agda?

Since IR increases proof theoretic strength, it is plausible that Agda can
prove all of Coq consistent. (Coq does not have IR)
 It seems that it would be possible only if all the universes of Coq can be
defined in just one universe of Agda. If the definition of a universe of
Coq jumped universe levels in Agda, one can only prove the consistency of
finitely many universes if Coq.


-- Abhishek
http://www.cs.cornell.edu/~aa755/

P.S.: Can one define all universes of Agda in Coq with Prop?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131125/f1a1db23/attachment.html