  In generic realizability for set theories, realizers treat unbounded
quantifiers generically. To this form of realizability, we add another layer of
extensionality by requiring that realizers ought to act extensionally on
realizers, giving rise to a realizability universe $\mathrm{V_{ex}}(A)$ in
which the axiom of choice in all finite types ${\sf AC}_{{\sf FT}}$ is
realized, where $A$ stands for an arbitrary partial combinatory algebra. This
construction furnishes 'inner models' of many set theories that additionally
validate ${\sf AC}_{{\sf FT}}$, in particular it provides a self-validating
semantics for $\sf CZF$ (Constructive Zermelo-Fraenkel set theory) and $\sf
IZF$ (Intuitionistic Zermelo-Fraenkel set theory). One can also add large set
axioms and many other principles.
