### Abstract

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.

Revisions made subsequent to the first version of this article added additional material on pseudofunctors, pseudonatural transformations, modifications, and equivalence of bicategories; the main thrust being to give a proof that a pseudofunctor is a biequivalence if and only if it can be extended to an equivalence of bicategories.

### License

BSD License

### History

July 22, 2021
  Added new material: "concrete bicategories" and "bicategory of categories". (revision 49d3aa43c180)
November 4, 2020
  Added new material on equivalence of bicategories, with associated changes. (revision 472cb2268826)
February 15, 2020
  Move ConcreteCategory.thy from Bicategory to Category3 and use it systematically. Make other minor improvements throughout. (revision a51840d36867)

### Topics

- Mathematics/Category theory

### Session Bicategory

- IsomorphismClass
- Prebicategory
- Bicategory
- Coherence
- CanonicalIsos
- Subbicategory
- InternalEquivalence
- Pseudofunctor
- Strictness
- InternalAdjunction
- PseudonaturalTransformation
- EquivalenceOfBicategories
- SpanBicategory
- Tabulation
- BicategoryOfSpans
- Modification
- ConcreteBicategory
- CatBicat

### Depends on

- Monoidal Categories

## Cite

×

Bicategory-AFP

    @article{Bicategory-AFP,
      author  = {Eugene W. Stark},
      title   = {Bicategories},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Bicategory.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jan 9, 2020 : Isabelle2019