Indexed type theories

In this paper, we define indexed type theories which are related to indexed (∞-)categories in the same way as (homotopy) type theories are related to (∞-)categories. We define several standard constructions for such theories including finite (co)limits, arbitrary (co)products, exponents, object classifiers, and orthogonal factorization systems. We also prove that these constructions are equivalent to their type theoretic counterparts such as Σ-types, unit types, identity types, finite higher inductive types, Π-types, univalent universes, and higher modalities.

Models of non-well-founded sets via an indexed final coalgebra theorem

The paper uses the formalism of indexed categories to recover the proof of a standard final coalgebra theorem, thus showing existence of final coalgebras for a special class of functors on finitely complete and cocomplete categories. As an instance of this result, we build the final coalgebra for the powerclass functor, in the context of a Heyting pretopos with a class of small maps. This is then proved to provide models for various non-well-founded set theories, depending on the chosen axiomatisation for the class of small maps.

More on Descent Theory for Schemes

In this paper we continue the investigation of some aspects of descent theory for schemes that was begun in [Mesablishvili, Appl. Categ. Structures]. Let 𝐒𝐂𝐇 be a category of schemes. We show that quasi-compact pure morphisms of schemes are effective descent morphisms with respect to 𝐒𝐂𝐇-indexed categories given by (i) quasi-coherent modules of finite type, (ii) flat quasi-coherent modules, (iii) flat quasi-coherent modules of finite type, (iv) locally projective quasicoherent modules of finite type. Moreover, we prove that a quasi-compact morphism of schemes is pure precisely when it is a stable regular epimorphism in 𝐒𝐂𝐇. Finally, we present an alternative characterization of pure morphisms of schemes.

Towards a Categorical Semantics of Type Classes

This is an exercise in the description of programming languages as indexed categories. Type classes have been introduced into functional programming languages to provide a uniform framework for ‘overloading’. We establish a correspondence between type classes and comprehension schemata in categories. A coherence result allows us to describe subclasses and implicit conversions between types.

A category-theoretic account of program modules

The type-theoretic explanation of modules proposed to date (for programming languages like ML) is unsatisfactory, because it does not capture that the evaluation of type-expressions is independent from the evaluation of program expressions. We propose a new explanation based on ‘programming languages as indexed categories’ and illustrate how ML can be extended to support higher order modules, by developing a category-theoretic semantics for a calculus of modules with dependent types. The paper also outlines a methodology, which may lead to a modular approach in the study of programming languages.