Re: query: models of CIC

Milad Niqui <milad@cs.kun.nl> · Mon, 27 Oct 2003 18:32:10 +0100

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

Dear Thorsten,

Thanks for the explanation and references. I have some further 
remarks/questions:

> I am not sure what you mean by a "set theoretic model": there is an
> old result by Reynolds which shows that there are no non-trivial
> set-theoritic models of impredicativity (in classical set theory).

I clarify my question. By set theoretical model I mean any extension of
constructive set theories of Aczel, based on subset collection or
different forms of power-set axiom [1].

[1] P. Aczel . On Relating Type Theoreis and Set theories. Proceedings 
of Types 98, LNCS 1257

 >  To construct an impredicative
> universe one observes that the subcategory of modest omega-sets 
> (where the ||- relation is injective) provide a good interpretation
> fro Prop. 

How do we intrepret the impredicative universe Set then? The
  elimination rules for types Prop and Set are not symmetric so I guess
we need some modification of subcategory of modes-sets to interpret
both. Can this be done in a straightforward way?

Regards,

Milad