Logical Structure on Inverse Functor Categories
Category Theory
2024-10-16 v1 Logic in Computer Science
Logic
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.
Cite
@article{arxiv.2410.11728,
title = {Logical Structure on Inverse Functor Categories},
author = {Marcelo Fiore and Chris Kapulkin and Yufeng Li},
journal= {arXiv preprint arXiv:2410.11728},
year = {2024}
}
Comments
44 pages; comments welcome