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建立。这使得我们能够在正确的抽象层次上对各种单子进行形式化推理。特别地，我们定义了内部于二范畴的单子范畴，并证明它是一价的。我们还定义了Eilenberg-Moore对象，并展示了Eilenberg-Moore范畴和Kleisli范畴都能够产生Eilenberg-Moore对象。最后，我们将单子和任意二范畴中的自由对应联系起来。我们的工作使用Coq和UniMath库进行了形式化。
相关内容
微信扫码咨询专知VIP会员