  Werner's set-theoretical model is one of the most intuitive models of ECC. 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 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.
