An Interpetation of Aczel's Constructive Set Theory in Nuprl Type Theory
Mark Bickford, Cornell Computer Science

In 1977 Peter Aczel gave an interpretation of constructive set theory (CZF) in
Martin-L\"of type theory. In 1986 he added the Regular Extension Axiom (REA) to prove
the existence of inductively defined sets such as the hereditarily countable sets,
and gave an interpretation of REA in Martin-L\"of type theory with W-types.
Later he studied a theory of non-wellfounded sets, where the foundation axiom
is replaced by an anti-foundation axiom.

We can carry out Aczel's interpretation of CZF, including the REA, in Nuprl.
By using a co-inductive version of the W-type that we call the co-W-type, we
can interpret Aczel's non-wellfounded sets. In fact, the
wellfounded sets are just a subtype of the non-wellfounded sets, so a single
interpretation works for both theories and unifies them. The interpretation of
equality on non-wellfounded sets is bisimulation, and the best way to define that
uses winning strategies for certain games. So we develop some constructive game theory.
A possibly new result is that the REA also holds for the non-wellfounded sets.