Monoidal closure of Grothendieck constructions via $Σ$-tractable monoidal structures and Dialectica formulas
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_ | 1866908613019172864 |
|---|---|
| author | Nunes, Fernando Lucatelli Vákár, Matthijs |
| author_facet | Nunes, Fernando Lucatelli Vákár, Matthijs |
| contents | We examine the categorical structure of the Grothendieck construction $Σ_{\mathsf{C}}\mathsf{L}$ of an indexed category $\mathsf{L} \colon \mathsf{C}^{op} \to \mathsf{CAT}$. Our analysis begins with characterisations of fibred limits, colimits, and monoidal (closed) structures. The study of fibred colimits leads naturally to a generalisation of the notion of extensive indexed category introduced in CHAD for Expressive Total Languages, and gives rise to the concept of left Kan extensivity, which provides a uniform framework for computing colimits in Grothendieck constructions.
We then establish sufficient conditions for the (non-fibred) monoidal closure of the total category $Σ_{\mathsf{C}}\mathsf{L}$. This extends Gödel's Dialectica interpretation and rests upon a new notion of $Σ$-tractable monoidal structure. Under this notion, $Σ$-tractable coproducts unify and extend cocartesian coclosed structures, biproducts, and extensive coproducts. Finally, we consider when the induced closed structure is fibred, showing that this need not hold in general, even in the presence of a fibred monoidal structure. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_07724 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Monoidal closure of Grothendieck constructions via $Σ$-tractable monoidal structures and Dialectica formulas Nunes, Fernando Lucatelli Vákár, Matthijs Category Theory Logic in Computer Science Programming Languages 18N10, 18C10, 18F10, 18A22, 18A40, 18D10, 03B70, 68Q55, 03F52, 03F03 F.3.2; F.3.3; F.4.1; F.1.1; G.2.2 We examine the categorical structure of the Grothendieck construction $Σ_{\mathsf{C}}\mathsf{L}$ of an indexed category $\mathsf{L} \colon \mathsf{C}^{op} \to \mathsf{CAT}$. Our analysis begins with characterisations of fibred limits, colimits, and monoidal (closed) structures. The study of fibred colimits leads naturally to a generalisation of the notion of extensive indexed category introduced in CHAD for Expressive Total Languages, and gives rise to the concept of left Kan extensivity, which provides a uniform framework for computing colimits in Grothendieck constructions. We then establish sufficient conditions for the (non-fibred) monoidal closure of the total category $Σ_{\mathsf{C}}\mathsf{L}$. This extends Gödel's Dialectica interpretation and rests upon a new notion of $Σ$-tractable monoidal structure. Under this notion, $Σ$-tractable coproducts unify and extend cocartesian coclosed structures, biproducts, and extensive coproducts. Finally, we consider when the induced closed structure is fibred, showing that this need not hold in general, even in the presence of a fibred monoidal structure. |
| title | Monoidal closure of Grothendieck constructions via $Σ$-tractable monoidal structures and Dialectica formulas |
| topic | Category Theory Logic in Computer Science Programming Languages 18N10, 18C10, 18F10, 18A22, 18A40, 18D10, 03B70, 68Q55, 03F52, 03F03 F.3.2; F.3.3; F.4.1; F.1.1; G.2.2 |
| url | https://arxiv.org/abs/2405.07724 |