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.

翻译：我们基于Street建立的单子形式理论，在单值基础（univalent foundations）框架下发展该理论。这使得我们能够在恰当的抽象层次对各类单子进行形式化推理。具体而言，我们定义了双范畴（bicategory）内部的单子双范畴，并证明其是单值的。同时定义了Eilenberg-Moore对象，并证明了无论是Eilenberg-Moore范畴还是Kleisli范畴都能导出Eilenberg-Moore对象。最后，我们在任意双范畴中建立了单子与伴随函子（adjunctions）之间的联系。本研究使用基于UniMath库的Coq证明助手完成了形式化实现。