License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2023.6
URN: urn:nbn:de:0030-drops-179904
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17990/
van der Weide, Niels
The Formal Theory of Monads, Univalently
Abstract
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 https://github.com/UniMath/UniMath library.
BibTeX - Entry
@InProceedings{vanderweide:LIPIcs.FSCD.2023.6,
author = {van der Weide, Niels},
title = {{The Formal Theory of Monads, Univalently}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {6:1--6:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/17990},
URN = {urn:nbn:de:0030-drops-179904},
doi = {10.4230/LIPIcs.FSCD.2023.6},
annote = {Keywords: bicategory theory, univalent foundations, formalization, monads, Coq}
}
