[FOM] Predicativity in CZF

[Nik Weaver]

Dan Mehkeri wrote:

> But "total relation from A to B" means: for every x in A there
> is at least one related element y in B. Reading intuitionistically,
> it is the superset of (the graph of) an certain intensional function
> from A to B. So if C were the set of intensional functions from A to
> B, then that would already be in C, so Fullness, therefore Subset
> Collection, would be validated. Of course this still depends on a
> function space construction, but we didn't need to assume any power
> sets.

What about the case where A is the natural numbers and B = {0,1}?
Drawing a distinction between intensional and extensional functions
doesn't seem to change matters because natural numbers have normal
forms, so you can canonically turn intensional functions into
extensional functions.

The set of extensional functions from N to {0,1} seems to me just
as impredicative as the power set of N.  Isn't that right?

Nik