<div dir="ltr"><div>(because of the relevance of this question to both Coq and Agda communities, I'm posting it to both lists.)</div><div><br></div><div>Hi,</div><div>I've been curious about the usefulness of induction recursion(IR)</div>
<div>in defining universes. The canonical use-case of Induction-Recursion</div><div>seems to be in defining a universe closed under dependent functions(PI).</div><div>One cool thing about the Inductive-Recursive formulation of such a universe is that it fits in Set 0</div>
<div>(the first universe of Agda(or any similar methatheory supporting IR)).</div><div><br></div><div>Converting this definition to an Inductive one makes its type jump to Set 1</div><div><div>(This was discussed in <a href="http://comments.gmane.org/gmane.science.mathematics.logic.coq.club/11380" target="_blank">http://comments.gmane.org/gmane.science.mathematics.logic.coq.club/11380</a>. see Andrew Cave's comment)<br>
</div></div><div><br></div><div>(When I mention Coq below, I really mean Coq without Prop.)</div><div><br></div><div>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.)</div>
<div>If so, does the definition fit in Set 0 of Agda? </div><div><br></div><div>Since IR increases proof theoretic strength, it is plausible that Agda can prove all of Coq consistent. (Coq does not have IR)</div><div> 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.</div>
<div><br></div><div><br></div><div><div>-- Abhishek</div><a href="http://www.cs.cornell.edu/~aa755/" target="_blank">http://www.cs.cornell.edu/~aa755/</a></div><div><br></div><div>P.S.: Can one define all universes of Agda in Coq with Prop?</div>
</div>