🔍

Equations Inline Footnotes

open import Cat.Bi.Instances.Functor
open import Cat.Bi.Functor.Constant
open import Cat.Functor.Naturality
open import Cat.Functor.Bifunctor
open import Cat.Bi.Functor.Base
open import Cat.Bi.Equivalence hiding (is-equivalence)
open import Cat.Bi.Functor.Hom
open import Cat.Functor.Base
open import Cat.Bi.Duality hiding (_^op)
open import Cat.Bi.Solver
open import Cat.Bi.Base
open import Cat.Prelude

import Cat.Bi.Reasoning as Br
import Cat.Reasoning as Cr

module Cat.Bi.Diagram.Colimit where

Bicategorical colimits🔗

private variable
  o h ℓ o' h' ℓ' : Level

module _
  {I : Prebicategory o h ℓ}
  {C : Prebicategory o' (o ⊔ h ⊔ ℓ ⊔ h' ⊔ ℓ') (o ⊔ h ⊔ ℓ ⊔ ℓ')}
  (F : Pseudofunctor I C)
  where

  open Prebicategory C
  open Pseudofunctor
  open Modification
  open Cr.Inverses
  open Cr._≅_
  open _=>ₗ_
  open _=>ₚ_
  open _=>_

Colimits are ubiquitous in category theory, describing universal constructions of a certain form. The same is true in bicategory theory, where we can consider diagrams given by pseudofunctors $F:\mathbf{I}\to \mathbf{C}\text{,}$ and colimiting objects $L\in \mathbf{C}$ such that any cocone over $F$ with apex $X$ corresponds to an essentially unique morphism $L\to X\text{.}$

The primary difference in dealing with bicategorical colimits compared to their 1-categorical counterparts is that commutativity requirements are relaxed to 2-cell isomorphisms. Bicategorical colimits are also more expressive in that the diagram can specify whether commutativity conditions should hold up to isomorphism or merely a directed transformation. For example, in a 1-category, given two parallel morphisms

we can consider a coequaliser, i.e., a universal morphism $h:B\to C$ identifying $f$ and $g$ in the sense that $hf=hg\text{.}$ In a bicategory we can consider a directed version of this construction, the coinserter, which consists of a universal 1-cell $h:B\to C$ equipped with a 2-cell $hf\Rightarrow hg\text{.}$

Other prominent examples of bicategorical colimits include, e.g, cocomma categories, localisations, and Kleisli categories.

Bicolimits and lax colimits🔗

To avoid having to define the machinery of cones or Kan extensions at the level of bicategories, we use the characterisation of colimits as representing objects. In 1-category theory, a functor $G:\mathcal{I}\to \mathcal{C}$ has a colimit $L$ if and only if there is an isomorphism $\mathcal{C}(L,X)\cong \mathbf{Nat}(G,{\Delta }_X)$ natural in $X\text{.}$ Similarly, in the setting of bicategories, we say that a pseudofunctor $F:\mathbf{I}\to \mathbf{C}$ has a bicolimit $L$ if and only if there is an equivalence of categories $\mathbf{C}(L,X)\cong [\mathbf{I},\mathbf{C}](F,{\Delta }_X)$ pseudonatural in $X\text{,}$ where $\mathbf{C}(L,-):\mathbf{C}\to \mathfrak{Cat}$ is the bicategorical Hom functor, ${\Delta }_X$ is the constant pseudofunctor at $X\text{,}$ and $[\mathbf{I},\mathbf{C}]$ is the bicategory of pseudofunctors from $\mathbf{I}$ to $\mathbf{C}\text{,}$ pseudonatural transformations between them, and modifications between those.

Recall that a natural transformation $\alpha :G\Rightarrow {\Delta }_X$ specifies a cocone over the functor $G\text{.}$ In the same way, a pseudonatural transformation $\phi :F\Rightarrow {\Delta }_X$ specifies a cocone over the pseudofunctor $F\text{,}$ illustrated in the diagram below.

For each object $i$ in the diagram, the map ${\phi }_i:F(i)\to X$ gives a leg of the cocone, and for any morphism $f:i\to j\text{,}$ we have an invertible 2-cell ${\nu }_f:{\phi }_i\cong {\phi }_{j}F(f)$ in place of the usual commutativity requirement for cocones.

As is often the case in bicategorical definitions, we have the choice of whether to consider cocones $F\to {\Delta }_X$ which commute strongly (so that ${\nu }_f$ is an isomorphism as above), or to take cocones with “directed” commutative squares (so that ${\nu }_f$ is a general 2-cell). The latter choice yields the notion of a lax colimit (or oplax, depending on the direction of the 2-cells). It is known that (op-)lax colimits can be expressed as bicolimits by altering the diagram category, but here we give a direct definition.

Defining lax colimits🔗

A lax colimit of a pseudofunctor $F:\mathbf{I}\to \mathbf{C}$ consists of an object $L$ in $\mathbf{C}$ together with a pseudonatural equivalence $\mathbf{C}(L,-)\cong [\mathbf{I},\mathbf{C}{]}_o(F,\Delta )\text{,}$ where $[\mathbf{I},\mathbf{C}{]}_o$ denotes the bicategory of pseudofunctors from $\mathbf{I}$ to $\mathbf{C}$ together with oplax transformations between them.¹ The codomain of this equivalence can be translated into Mikan as follows.

  lax-cocones-at : Pseudofunctor C (Cat _ _)
  lax-cocones-at = Hom-from-bi (Pseudoₒ I C) (opᵖ F) P∘ Const-pseudoₒ

Now, by a bicategorical Yoneda argument, any pseudonatural equivalence of the form above is determined by its value at $\mathrm{id}:L\to L\text{,}$ which is a cocone $F\Rightarrow {\Delta }_L\text{,}$ namely the universal colimiting cocone. Conversely, any cocone at $L$ induces a functor $\mathbf{C}(L,X)\to [\mathbf{I},\mathbf{C}{]}_o(F,{\Delta }_L)$ by precomposition.

  module _ (L : Ob) (univ-cocone : opᵖ F .lax =>ₒ ConstP L .lax) where

    hom→cocone₀ : (X : Ob) → Functor (Hom L X) Pseudoₒ[ opᵖ F , ConstP X ]
    hom→cocone₀ X =
         preaction (Pseudoₒ _ _) {opᵖ F} {ConstP L} {ConstP X} univ-cocone
      F∘ Const-pseudoₒ.Const₁

    module _ {X Y : Ob} where
      hom→cocone-nat
        :  preaction (Cat _ _) (hom→cocone₀ Y)
        F∘ Flip (Lax.compose _ _) F∘ Const-pseudoₒ.Const₁
        ≅ⁿ postaction (Cat _ _) (hom→cocone₀ X) F∘ compose
      hom→cocone-nat = to-natural-iso ni where
        open make-natural-iso
        ni : make-natural-iso _ _
        ni .eta f .η g .Γ a         = α← _
        ni .eta f .η g .is-natural  = bicat! C
        ni .eta f .is-natural g h α = ext λ _ → bicat! C
        ni .inv f .η g .Γ a         = α→ _
        ni .inv f .η g .is-natural  = bicat! C
        ni .inv f .is-natural g h α = ext λ _ → bicat! C
        ni .eta∘inv f               = ext λ _ _ → Br.α≅ C .invr
        ni .inv∘eta f               = ext λ _ _ → Br.α≅ C .invl
        ni .natural g h α           = ext λ _ _ → bicat! C

    hom→cocone : Hom-from-bi C L .lax =>ₚ lax-cocones-at .lax
    hom→cocone .lax .σ                = hom→cocone₀
    hom→cocone .lax .naturator        = hom→cocone-nat .to
    hom→cocone .lax .ν-compositor f g = ext λ _ _ → bicat! C
    hom→cocone .lax .ν-unitor         = ext λ _ _ → bicat! C
    hom→cocone .naturator-inv f       =
      Cr.iso→invertible Cat[ _ , _ ] (isoⁿ→iso hom→cocone-nat f)

In other words, to show that $L$ is the lax colimit of $F\text{,}$ it suffices to provide a candidate cocone with apex $L\text{,}$ and show that the induced hom→cocone is a pseudonatural equivalence, which corresponds to showing that the provided cocone is universal.

    is-lax-colimit : Type _
    is-lax-colimit = is-equivalenceᵖ hom→cocone