论文标题
单调的形式理论
The Formal Theory of Monads, Univalently
论文作者
论文摘要
我们在街头基础上开发了街头的正式理论。这使我们能够正式推理在正确的抽象级别上的各种单子。特别是，我们定义了生物体内部的Monads的生物，并证明它是无数的。我们还定义了Eilenberg-Moore对象，我们表明Eilenberg-Moore类别和Kleisli类别都会引起Eilenberg-Moore对象。最后，我们将任意生物游戏中的单子和套件联系起来。我们的工作使用Unimath库在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 UniMath library.
