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 “ ${\tt Prop}$ ”. However, this model of ${\tt Prop}$ is so coarse that the principle of excluded middle $P \lor \neg P$ holds. Following our previous work, we interpret ${\tt 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 ${\mathsf{list}}$ s.

In this paper, we study quasi-metric spaces using domain theory. Given a quasi-metric space (X,d), we use $({\bf B}(X,d),\leq^{d^{+}}\!)$ to denote the poset of formal balls of the associated quasi-metric space (X,d). We introduce the notion of local Yoneda-complete quasi-metric spaces in terms of domain-theoretic properties of $({\bf B}(X,d),\leq^{d^{+}}\!)$ . The manner in which this definition is obtained is inspired by Romaguera–Valero theorem and Kostanek–Waszkiewicz theorem. Furthermore, we obtain characterizations of local Yoneda-complete quasi-metric spaces via local nets in quasi-metric spaces. More precisely, we prove that a quasi-metric space is local Yoneda-complete if and only if every local net has a d-limit. Finally, we prove that every quasi-metric space has a local Yoneda completion.

Jacobs has proposed definitions for (weak, strong, split) generic objects for a fibered category; building on his definition of (split) generic objects, Jacobs develops a menagerie of important fibrational structures with applications to categorical logic and computer science, including higher order fibrations, polymorphic fibrations, $\lambda2$ -fibrations, triposes, and others. We observe that a split generic object need not in particular be a generic object under the given definitions, and that the definitions of polymorphic fibrations, triposes, etc. are strict enough to rule out some fundamental examples: for instance, the fibered preorder induced by a partial combinatory algebra in realizability is not a tripos in this sense. We propose a new alignment of terminology that emphasizes the forms of generic object appearing most commonly in nature, i.e. in the study of internal categories, triposes, and the denotational semantics of polymorphism. In addition, we propose a new class of acyclic generic objects inspired by recent developments in higher category theory and the semantics of homotopy type theory, generalizing the realignment property of universes to the setting of an arbitrary fibration.