单值化基础下的幺半群形式理论
计算机科学中的逻辑
2025-02-26 v7 范畴论
摘要
我们在单值化基础（univalent foundations）下发展了由Street建立的幺半群（monad）形式理论。这使我们能够在正确的抽象层次上对各种幺半群进行形式推理。特别地，我们定义了二元范畴（bicategory）内部的幺半群二元范畴，并证明它是单值化的。我们还定义了Eilenberg-Moore对象，并证明Eilenberg-Moore范畴与Kleisli范畴均给出Eilenberg-Moore对象。最后，我们在任意二元范畴中关联了幺半群与伴随。我们的工作使用UniMath库在Coq中形式化。
引用
@article{arxiv.2212.08515,
title = {The Formal Theory of Monads, Univalently},
author = {Niels van der Weide},
journal= {arXiv preprint arXiv:2212.08515},
year = {2025}
}