The Formal Theory of Monads, Univalently
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2022
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866916629231697920 |
|---|---|
| author | van der Weide, Niels |
| author_facet | van der Weide, Niels |
| contents | We develop the formal theory of monads, as established by Street, in univalent foundations. This allows us to formally reason about various kinds of monads on the right level of abstraction. In particular, we define the bicategory of monads internal to a bicategory, and prove that it is univalent. We also define Eilenberg-Moore objects, and we show that both Eilenberg-Moore categories and Kleisli categories give rise to Eilenberg-Moore objects. Finally, we relate monads and adjunctions in arbitrary bicategories. Our work is formalized in Coq using the UniMath library. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2212_08515 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | The Formal Theory of Monads, Univalently van der Weide, Niels Logic in Computer Science Category Theory We develop the formal theory of monads, as established by Street, in univalent foundations. This allows us to formally reason about various kinds of monads on the right level of abstraction. In particular, we define the bicategory of monads internal to a bicategory, and prove that it is univalent. We also define Eilenberg-Moore objects, and we show that both Eilenberg-Moore categories and Kleisli categories give rise to Eilenberg-Moore objects. Finally, we relate monads and adjunctions in arbitrary bicategories. Our work is formalized in Coq using the UniMath library. |
| title | The Formal Theory of Monads, Univalently |
| topic | Logic in Computer Science Category Theory |
| url | https://arxiv.org/abs/2212.08515 |