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

Peter Hancock hancock at spamcop.net
Tue Nov 26 15:37:35 CET 2013

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
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.


More information about the Agda mailing list