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

Cite as @fiore-2024-logical (helia, typst) · \cite{fiore-2024-logical} (LaTeX)
BibTeX
bibtex · 8 lines
@misc{fiore-2024-logical,
  author = {Marcelo P. Fiore and Chris Kapulkin and Yufeng Li},
  title = {Logical Structure on Inverse Functor Categories},
  year = {2024},
  month = {10},
  eprint = {2410.11728},
  archiveprefix = {arXiv}
}
hayagriva YAML (typst)
yaml · 10 lines
fiore-2024-logical:
  type: misc
  title: Logical Structure on Inverse Functor Categories
  author:
  - Fiore, Marcelo P.
  - Kapulkin, Chris
  - Li, Yufeng
  date: 2024-10
  serial-number:
    arxiv: '2410.11728'
fiore-2024-logical reference entries/refs/fiore-2024-logical/fiore-2024-logical.hel