The Frobenius equivalence and Beck-Chevalley condition for Algebraic Weak Factorisation Systems
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914767951626240 |
|---|---|
| author | van Woerkom, Wijnand Berg, Benno van den |
| author_facet | van Woerkom, Wijnand Berg, Benno van den |
| contents | If a locally cartesian closed category carries a weak factorisation system, then the left maps are stable under pullback along right maps if and only if the right maps are closed under pushforward along right maps. We refer to this statement as the Frobenius equivalence and in this paper we state and prove an analogical statement for algebraic weak factorisation systems. These algebraic weak factorisation systems are an explicit variant of the more traditional weak factorisation systems in that the factorisation and the lifts are part of the structure of an algebraic weak factorisation system and are not merely required to exist. Our work has been motivated by the categorical semantics of type theory, where the Frobenius equivalence provides a useful tool for constructing dependent function types. We illustrate our ideas using split fibrations of groupoids, which are the backbone of the groupoid model of Hofmann and Streicher. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_15443 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | The Frobenius equivalence and Beck-Chevalley condition for Algebraic Weak Factorisation Systems van Woerkom, Wijnand Berg, Benno van den Category Theory Logic 18A32, 18N10, 03B38 If a locally cartesian closed category carries a weak factorisation system, then the left maps are stable under pullback along right maps if and only if the right maps are closed under pushforward along right maps. We refer to this statement as the Frobenius equivalence and in this paper we state and prove an analogical statement for algebraic weak factorisation systems. These algebraic weak factorisation systems are an explicit variant of the more traditional weak factorisation systems in that the factorisation and the lifts are part of the structure of an algebraic weak factorisation system and are not merely required to exist. Our work has been motivated by the categorical semantics of type theory, where the Frobenius equivalence provides a useful tool for constructing dependent function types. We illustrate our ideas using split fibrations of groupoids, which are the backbone of the groupoid model of Hofmann and Streicher. |
| title | The Frobenius equivalence and Beck-Chevalley condition for Algebraic Weak Factorisation Systems |
| topic | Category Theory Logic 18A32, 18N10, 03B38 |
| url | https://arxiv.org/abs/2404.15443 |