一句话：在单值基础中形式化 Street 的单子理论，构造内蕴单子双范畴并证明其单值性，全部结果由 Coq/UniMath 机器验证。
本文在单值基础（univalent foundations）中发展 Street 所建立的形式单子理论，以便在恰当的抽象层次上形式化推理各类单子。作者定义任意双范畴内部单子构成的双范畴，并证明该双范畴是单值的；随后定义 Eilenberg-Moore 对象，证明 Eilenberg-Moore 范畴与 Kleisli 范畴都可产生 Eilenberg-Moore 对象；最后在任意双范畴中建立单子与伴随之间的关联。全部结果在 Coq 中使用 UniMath 库机器化验证。
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.