Werner's set-theoretical model is one of the simplest models of CIC. It\ncombines a functional view of predicative universes with a collapsed view of\nthe impredicative sort Prop. However this model of Prop is so coarse that the\nprinciple of excluded middle holds. Following our previous work, we interpret\nProp into a topological space (a special case of Heyting algebra) to make the\nmodel more intuitionistic without sacrificing simplicity. We improve on that\nwork by providing a full interpretation of dependent product types, using\nAlexandroff spaces. We also extend our approach to inductive types by adding\nsupport for lists.\n