Logical Structure on Inverse Functor Categories

TL;DR

This paper explores when logical structures like dependent products and subobject classifiers can be transferred from a base category to diagram categories, with conditions involving homotopical localizations.

Contribution

It provides new conditions under which logical structures are induced in inverse functor categories, extending categorical semantics for dependent type theories.

Findings

Conditions for transferring logical structures to diagram categories

Analysis of localization effects on presheaf categories

Connections between homotopical localizations and logical structure preservation

Abstract

Inspired by recent work on the categorical semantics of dependent type theories, we investigate the following question: When is logical structure (crucially, dependent-product and subobject-classifier structure) induced from a category to categories of diagrams in it? Our work offers several answers, providing a variety of conditions on both the category itself and the indexing category of diagrams. Additionally, motivated by homotopical considerations, we investigate the case when the indexing category is equipped with a class of weak equivalences and study conditions under which the localization map induces a structure-preserving functor between presheaf categories.