An Intuitionistic Set-theoretical Model of CCω
Masahiro Sato, Jacques Garrigue · Journal of Information Processing · 2016
Werner's set-theoretical model is one of the simplest models of CC ω.It combines a functional view of predicative universes with a collapsed view of the impredicative sort Prop.However this model of Prop is so coarse that the principle of excluded middle P ∨ ¬P holds.In this paper, we interpret Prop into a topological space (a special case of Heyting algebra) to make it more intuitionistic without sacrificing simplicity.We prove soundness and show some applications of our model.