2026-07-24T22:06:32Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17990 2024-03-06T11:00:48Z ddc:004 open_access

The Formal Theory of Monads, Univalently van der Weide, Niels bicategory theory univalent foundations formalization monads Coq 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Niels van der Weide 2023 Is Part Of LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2023.6 urn:nbn:de:0030-drops-179904 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.6 eng https://creativecommons.org/licenses/by/4.0/legalcode