An Intuitionistic Set-theoretical Model of Fully Dependent CC{\omega}

TL;DR

This paper introduces an intuitionistic set-theoretical model of CIC{ extomega} that refines Werner's model by interpreting Prop in topological spaces and extending it to dependent types and inductive lists.

Contribution

It provides a fully interpreted dependent product and inductive types within an intuitionistic framework using Alexandroff spaces, improving prior models.

Findings

Interpretation of Prop in topological spaces enhances intuitionism.

Full interpretation of dependent product types using Alexandroff spaces.

Extension to inductive types with support for lists.

Abstract

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.