Indexed type theories

TL;DR

This paper introduces indexed type theories, establishing their relation to indexed (infinity-)categories and demonstrating that standard categorical constructions correspond to key type-theoretic features.

Contribution

It defines indexed type theories and proves their constructions are equivalent to fundamental type-theoretic concepts like $ ext{Sigma}$-types, identity types, and univalent universes.

Findings

Indexed type theories relate to indexed (infinity-)categories.

Standard categorical constructions correspond to type-theoretic features.

Equivalence between categorical and type-theoretic constructions established.

Abstract

In this paper, we define indexed type theories which are related to indexed ($\infty$-)categories in the same way as (homotopy) type theories are related to ($\infty$-)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 $\Sigma$-types, unit types, identity types, finite higher inductive types, $\Pi$-types, univalent universes, and higher modalities.