[Prev][Next][Index][Thread]
Re: query: models of CIC
[----- 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