Re: query: models of CIC
[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
Thanks for the explanation and references. I have some further
> 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 .
 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?