2010/09/18 by Berg, Benno van den, Moerdijk, Ieke
#03F50 #18F10 #18F20 #Category Theory (math.CT) #FOS: Mathematics #Logic (math.LO)
paper · doi:10.48550/arxiv.1009.3553
We show how one may establish proof-theoretic results for constructive Zermelo-Fraenkel set theory, such as the compactness rule for Cantor space and the Bar Induction rule for Baire space, by constructing sheaf models and using their preservation properties.