Reference. Logical Structure on Inverse Functor Categories
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
Cites 8 works (0 here)
External (8)
- Homotopical inverse diagrams in categories with attributes (2021)
- Reedy categories and their generalizations (2015)
- The theory and practice of Reedy categories (2014)
- Univalence for inverse diagrams and homotopy canonicity (2014)
- On an extension of the notion of Reedy category (2010)
- The Comprehensive factorisation and torsors (2010)
- Sheaves in Geometry and Logic: A First Introduction to Topos Theory (1994)
- Intuitionist type theory and the free topos (1980)