  Werner's set-theoretical model is one of the simplest models of CIC. 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. Following our previous work, we interpret
Prop into a topological space (a special case of Heyting algebra) to make the
model more intuitionistic without sacrificing simplicity. We improve on that
work by providing a full interpretation of dependent product types, using
Alexandroff spaces. We also extend our approach to inductive types by adding
support for lists.
