with Coquand, T. , 2012, A computational interpretation of forcing in type theory, in P. Dybjer, S. Lindström, E. Palmgren & G. Sundholm (eds.), Epistemology versus ontology, Dordrecht, Springer, pp. 203-213.