Re: [TYPES] independence of AC! or AC from CIC

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Milly,

my model in loc.cit. interpretates types as assemblies and thus all
inductive types as required by ICC. Only Prop is interpreted alternatively
in order to falsify Axiom of Unique Choice.

Thomas

> is it known whether the axiom of unique choice  (AC!)  or even
> the only axiom of choice (both as formulas in Prop)
>
> are independent from the Calculus of Inductive Constructions ?
>
> Any reference?
>
> For the pure Calculus of Constructions the  independence of AC! and AC
> was shown
> in
> T. Streicher " Independence of the induction principle and the axiom of
> choice in the pure calculus of constructions." TCS, 1992, vol.103.
>
> Many thanks for your cooperation
> Milly
> (Maria Emilia Maietti)
>