[FOM] Nonconservative law of excluded middle

[hendrik@topoi.pooq.com]

On Thu, May 01, 2008 at 09:51:22PM -0400, Daniel Méhkeri wrote:
>
> On the other hand it seems that this is not so for
> Aczel's constructive set theory (CZF). CZF is
> interpretable in an extension of Martin-Löf
> type-theory (augmented with "W-types"), though I don't
> claim to understand this interpretation.

This I didn't know.  Could you provide a reference?
(preferably on-line; I don't have easy access to a library)

-- hendrik

> ...
> ...
> Whew! This is a pretty spectacular non-conservativity!

Spectacular enough that I'd like to see the details here, too.

-- hendrik