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

[Peter Hancock]

On 25/11/2013 23:38, Abhishek Anand wrote:
..
> (When I mention Coq below, I really mean Coq without Prop.)
..
> P.S.: Can one define all universes of Agda in Coq with Prop?

A number of horribly smart
people have been thinking about the strength of Coq, and similar/related
type theories with some kind of impredicative powerset/full separation operation.
So far, with no definite answer.
I just want to recommend the paper
http://www1.maths.leeds.ac.uk/~rathjen/ML-Beitrag_Chapter_15-Buch.pdf
which has a brief survey over or intro to (part of) the general area.
Maybe also Alexandre Miquel has written something relevant.

My vague impression is that the strength of Coq is somewhere "north" of
(intuitionistic) Zermelo's set theory (and so way way stronger than IR).
But as for using this strength to actually emulate IR in a practically
useful way, I've no real idea.
Anton Setzer has modelled IR using ZF with a Mahlo cardinal, and the model
probably doesn't need full ZF, but probably only KP set theory + a recursively
Mahlo cardinal.

Peter