Logical Structure on Inverse Functor Categories
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914973746200576 |
|---|---|
| author | Fiore, Marcelo Kapulkin, Chris Li, Yufeng |
| author_facet | Fiore, Marcelo Kapulkin, Chris Li, Yufeng |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_11728 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Logical Structure on Inverse Functor Categories Fiore, Marcelo Kapulkin, Chris Li, Yufeng Category Theory Logic in Computer Science Logic 18A25, 18N55, 03G30 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. |
| title | Logical Structure on Inverse Functor Categories |
| topic | Category Theory Logic in Computer Science Logic 18A25, 18N55, 03G30 |
| url | https://arxiv.org/abs/2410.11728 |