arXiv · 2410.11728
Logical Structure on Inverse Functor Categories
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.
Explore related subjects
Keep this discovery
Marcelo Fiore, Chris Kapulkin, Yufeng Li. 2024-10-15. Logical Structure on Inverse Functor Categories. https://arxiv.org/abs/2410.11728
Cite the original work for its findings. Save a collection to share your selection of sources.