Re: query: models of CIC

Thomas Streicher <streicher@mathematik.tu-darmstadt.de> · Tue, 28 Oct 2003 12:15:19 +0100 (CET)

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

Dear Milad,

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

well, one can certainly perform realizability model construction in CZF
but the PER will not be impredicative anymore; that should not affect the
semantics of inductive types, however; in the Thesis of Anton Setzer (and
probably in published material of his thesis as well) he constructed 
realizability semantics for MLTT with one universe and W-types based on some
form of Kripke-Platek set theory;

but maybe you rather ask the question to which extent the usual set-theoretic
constructions of inductive types go through in CZF; there is certainly a limit
to that because CZF can be interpreted in MLTT with one universe and W-types
(as shown by Aczel in the late 1970ies)

Best, Thomas