Abstract

CZF is Peter Aczel's constructive set theory, his compromise between the familiar yet "cloudy" language of ZF and the concrete yet "scratchy" bedrock of intuitionistic type theory. In this introductory talk, I will walk through the development of CZF, starting at the very bottom---with the well-founded-tree construction that grounds everything in computational type theory---and working up through the basic propositions to the ZF-like axioms.