Email Gateway (Aug 22 2022 at 21:13): Email Gateway (Aug 22 2022 at 21:13):From: Tobias Nipkow <nipkow@in.tum.de>
Bicategories
Eugene W. Stark
Taking as a starting point the author's previous work on developing aspects of
category theory in Isabelle/HOL, this article gives a compatible formalization
of the notion of "bicategory" and develops a framework within which formal
proofs of facts about bicategories can be given. The framework includes a number
of basic results, including the Coherence Theorem, the Strictness Theorem,
pseudofunctors and biequivalence, and facts about internal equivalences and
adjunctions in a bicategory. As a driving application and demonstration of the
utility of the framework, it is used to give a formal proof of a theorem, due to
Carboni, Kasangian, and Street, that characterizes up to biequivalence the
bicategories of spans in a category with pullbacks. The formalization effort
necessitated the filling-in of many details that were not evident from the brief
presentation in the original paper, as well as identifying a few minor
corrections along the way.
https://www.isa-afp.org/entries/Bicategory.html
Enjoy this first contribution in 2020, and the second-largest entry in the AFP!
smime.p7s
Last updated: Oct 31 2025 at 16:27 UTC