Contextually indexed contextual categories

TL;DR

This paper introduces a generalized framework called contextually indexed categories, extending models of type theories and establishing their properties within certain model categories, including simplicial sets.

Contribution

It defines contextually indexed categories, generalizes type-theoretic semi-fibration categories, and demonstrates their realization in the Joyal model structure for simplicial sets.

Findings

Every model category with cofibrations stable under pullbacks forms a type-theoretic semi-fibration category.

Such categories give rise to contextually indexed contextual categories with finite limits.

The category of simplicial sets with the Joyal model structure forms a locally small Cartesian closed contextually indexed category.

Abstract

In this paper, we define a generalization of indexed categories and contextual categories which we call contextually indexed (contextual) categories. While contextual categories are models of ordinary type theories, contextually indexed (contextual) categories are models of indexed type theories. We also define type-theoretic semi-fibration categories which generalize type-theoretic fibration categories. Every model category in which cofibrations are stable under pullbacks is a type-theoretic semi-fibration category. We show that type-theoretic semi-fibration category gives rise to a contextually indexed contextual category with finite limits. Finally, we prove that the category of simplicial sets with the Joyal model structure gives rise to a locally small Cartesian closed contextually indexed contextual category with indexed limits and colimits.