A Normalizing Intuitionistic Set Theory with Inaccessible Sets
No Access Until
Permanent Link(s)
Other Titles
Author(s)
Abstract
We propose a set theory strong enough to interpret powerful type
theories underlying proof assistants such as LEGO and also possibly Coq, which at the same time enables program extraction from constructive proofs. For this purpose, we axiomatize impredicative constructive version of Zermelo-Fraenkel set theory IZF with Replacement and