open import Cat.Instances.Functor
open import Cat.Instances.Product
open import Cat.Functor.Hom
open import Cat.Prelude

import Cat.Functor.Bifunctor as Bi
import Cat.Functor.Reasoning as Fr
import Cat.Reasoning as Cr

module Cat.Bi.Base where


A (pre)bicategory is the natural higher-dimensional generalisation of a (pre)category. Whereas a precategory has Hom\hom-sets, a prebicategory has Hom\hom-precategories. While this generalisation might seem simple, in reality, we must be very careful when setting up the resulting structure: The key observation is that precategories have no notion of equality of objects, so everything which was an equation in the definition of precategories must be replaced with (sufficiently coherent) specified isomorphisms.

The data of a prebicategory consists of a type of objects Ob\bf{Ob}, and for each A,B:ObA, B : \bf{Ob}, a precategory Hom(A,B)\hom(A, B). We refer to the type of objects of Hom(A,B)\hom(A, B) by A↦BA \mapsto B, and call its inhabitants maps or 1-cells; In the second dimension, between each pair of maps f,gf, g, we have a set of 2-cells (sometimes homotopies), written f⇒gf \To g.

The composition operation of Hom(A,B)\hom(A,B), called vertical composition, will be written α⊗β\alpha \otimes \beta. As for why it’s called vertical composition, note that it reduces pasting diagrams of the form

record Prebicategory o ℓ ℓ′ : Type (lsuc (o ⊔ ℓ ⊔ ℓ′)) where
    Ob  : Type o
    Hom : Ob → Ob → Precategory ℓ ℓ′

  module Hom {A} {B} = Cr (Hom A B)

Zooming out to consider the whole bicategory, we see that each object has a specified identity 1-cell as in the case for ordinary categories, but the composition operation, rather than being a function, is a functor. This, intuitively, makes sense: since we have replaced our Hom\hom-sets with Hom\hom-precategories, we should replace our maps of sets for maps of precategories, i.e., functors.

    id      : ∀ {A} → Precategory.Ob (Hom A A)
    compose : ∀ {A B C} → Functor (Hom B C ×ᶜ Hom A B) (Hom A C)

  module compose {a} {b} {c} = Functor (compose {a} {b} {c})

Before moving on to the isomorphisms witnessing identity and associativity, we introduce a bunch of notation for the different classes of maps and all the composition operations. Observe that the action of the composition functor on homotopies reduces “horizontal” pasting diagrams like

whence the name horizontal composition.

  _↦_ : Ob → Ob → Type ℓ
  A ↦ B = Precategory.Ob (Hom A B)

  _⇒_ : ∀ {A B} (f g : A ↦ B) → Type ℓ′
  _⇒_ {A} {B} f g = Hom.Hom f g

  -- 1-cell composition
  _∘_ : ∀ {A B C} (f : B ↦ C) (g : A ↦ B) → A ↦ C
  f ∘ g = compose .Functor.F₀ (f , g)

  -- vertical 2-cell composition
  _⊗_ : ∀ {A B} {f g h : A ↦ B} → g ⇒ h → f ⇒ g → f ⇒ h
  _⊗_ {A} {B} = Hom._∘_

  -- horizontal 2-cell composition
  _◆_ : ∀ {A B C} {f₁ f₂ : B ↦ C} (β : f₁ ⇒ f₂) {g₁ g₂ : A ↦ B} (α : g₁ ⇒ g₂)
      → (f₁ ∘ g₁) ⇒ (f₂ ∘ g₂)
  _◆_ β α = compose .Functor.F₁ (β , α)

  infixr 30 _∘_
  infixr 25 _⊗_

  -- whiskering on the right
  _▶_ : ∀ {A B C} (f : B ↦ C) {a b : A ↦ B} (g : a ⇒ b) → f ∘ a ⇒ f ∘ b
  _▶_ {A} {B} {C} f g = compose .Functor.F₁ ( , g)

  -- whiskering on the left
  _◀_ : ∀ {A B C} {a b : B ↦ C} (g : a ⇒ b) (f : A ↦ B) → a ∘ f ⇒ b ∘ f
  _◀_ {A} {B} {C} g f = compose .Functor.F₁ (g ,

We now move onto the invertible 2-cells witnessing that the chosen identity map is a left- and right- unit element for the composition functor, and that composition is associative. In reality, to get a fully coherent structure, we need these invertible 2-cells to be given as natural isomorphisms, e.g. (id∘−)Id(\id{id} \circ -) \id{Id}, which witnesses that the functor “compose with the identity 1-cell on the left” is naturally isomorphic to the identity functor.

    unitor-l : ∀ {A B} → Cr._≅_ Cat[ Hom A B , Hom A B ] Id (Bi.Right compose id)
    unitor-r : ∀ {A B} → Cr._≅_ Cat[ Hom A B , Hom A B ] Id (Bi.Left compose id)

      : ∀ {A B C D}
      → Cr._≅_ Cat[ Hom C D ×ᶜ Hom B C ×ᶜ Hom A B , Hom A D ]
        (compose-assocˡ {H = Hom} compose)
        (compose-assocʳ {H = Hom} compose)

It’s traditional to refer to the left unitor as λ\lambda, to the right unitor as ρ\rho, and to the associator as α\alpha, so we set up those abbreviations here too:

  λ← : ∀ {A B} (f : A ↦ B) → id ∘ f ⇒ f
  λ← = unitor-l .Cr._≅_.from .η

  λ→ : ∀ {A B} (f : A ↦ B) → f ⇒ id ∘ f
  λ→ = unitor-l .Cr._≅ .η

  ρ← : ∀ {A B} (f : A ↦ B) → f ∘ id ⇒ f
  ρ← = unitor-r .Cr._≅_.from .η

  ρ→ : ∀ {A B} (f : A ↦ B) → f ⇒ f ∘ id
  ρ→ = unitor-r .Cr._≅ .η

  α→ : ∀ {A B C D} (f : C ↦ D) (g : B ↦ C) (h : A ↦ B)
     → (f ∘ g) ∘ h ⇒ f ∘ (g ∘ h)
  α→ f g h = associator .Cr._≅ .η (f , g , h)

  α← : ∀ {A B C D} (f : C ↦ D) (g : B ↦ C) (h : A ↦ B)
     → f ∘ (g ∘ h) ⇒ (f ∘ g) ∘ h
  α← f g h = associator .Cr._≅_.from .η (f , g , h)

The final data we need are coherences relating the left and right unitors (the triangle identity, nothing to do with adjunctions), and one for reducing sequences of associators, the pentagon identity. As for where the name “pentagon” comes from, the path pentagon witnesses commutativity of the diagram

      : ∀ {A B C} (f : B ↦ C) (g : A ↦ B)
      → (ρ← f ◀ g) ⊗ α← f id g ≡ f ▶ λ← g

      : ∀ {A B C D E} (f : D ↦ E) (g : C ↦ D) (h : B ↦ C) (i : A ↦ B)
      → (α← f g h ◀ i) ⊗ α← f (g ∘ h) i ⊗ (f ▶ α← g h i)
      ≡ α← (f ∘ g) h i ⊗ α← f g (h ∘ i)

Our coherence diagrams for bicategorical data are taken from (Leinster 1998), which contains all the diagrams we have omitted. However, we do not adopt their (dated) terminology of “homomorphism” and “strict homomorphism”. In contrast with our convention for 1-categories, we refer to bicategories using bold capital letters: B\bf{B}, C\bf{C}.

The bicategory of categories🔗

Just like the prototypal example of categories is the category of sets, the prototypal example of bicategory is the bicategory of categories. We observe that, without a bound of h-level on the spaces of objects (strict categories), the collection of categories of a given universe level does not form a category, but it does form a bicategory.

Cat : ∀ o ℓ → Prebicategory (lsuc o ⊔ lsuc ℓ) (o ⊔ ℓ) (o ⊔ ℓ)
Cat o ℓ = pb where
  open Prebicategory
  open Functor

  pb : Prebicategory _ _ _
  pb .Ob = Precategory o ℓ
  pb .Hom = Cat[_,_]
  pb .id = Id

The first thing we must compute is that the functor composition operator −∘−- \circ - extends to a functor composition functor, which is annoying but straightforward.

  pb .compose .F₀ (F , G) = F F∘ G

  pb .compose {C = C} .F₁ {y = y , _} (n1 , n2) .η x =
    y .F₁ (n2 .η _) C.∘ n1 .η _
    where module C = Precategory C

  pb .compose {C = C} .F₁ {x = F , G} {y = W , X} (n1 , n2) .is-natural _ _ f =
    (W .F₁ (n2 .η _) C.∘ n1 .η _) C.∘ F .F₁ (G .F₁ f) ≡⟨ C.pullr (n1 .is-natural _ _ _) ⟩≡
    W .F₁ (n2 .η _) C.∘ W .F₁ (G .F₁ f) C.∘ n1 .η _   ≡⟨ C.extendl (W.weave (n2 .is-natural _ _ _)) ⟩≡
    W .F₁ (X .F₁ f) C.∘ W .F₁ (n2 .η _) C.∘ n1 .η _   ∎
    where module C = Cr C
          module W = Fr W

  pb .compose {C = C} .F-id {x} = Nat-path λ _ → Cr.idr C _ ∙ x .fst .F-id
  pb .compose {C = C} .F-∘ {x} {y} {z} f g = Nat-path λ _ →
    z .fst .F₁ _ C.∘ f .fst .η _ C.∘ g .fst .η _                      ≡⟨ C.pushl (z .fst .F-∘ _ _) ⟩≡
    z .fst .F₁ _ C.∘ z .fst .F₁ _ C.∘ f .fst .η _ C.∘ g .fst .η _     ≡⟨ C.extend-inner (sym (f .fst .is-natural _ _ _)) ⟩≡
    z .fst .F₁ _ C.∘ f .fst .η _ C.∘ y .fst .F₁ _ C.∘ g .fst .η _     ≡⟨ solve C ⟩≡
    (z .fst .F₁ _ C.∘ f .fst .η _) C.∘ (y .fst .F₁ _ C.∘ g .fst .η _) ∎
    where module C = Cr C

The unitors and associator are given in components by the identity 2-cells, since componentwise the functor composition Id∘F\id{Id} \circ F evaporates, leaving only FF behind. Unfortunately, this equation is not definitional, so we can not use the identity natural isomorphism directly:

  pb .unitor-r {B = B} = to-natural-iso ni where
    module B = Cr B
    ni : make-natural-iso _ _
    ni .make-natural-iso.eta x = NT (λ _ → λ _ _ _ →
    ni .make-natural-iso.inv x = NT (λ _ → λ _ _ _ →
    ni .make-natural-iso.eta∘inv x = Nat-path λ _ → B.idl _
    ni .make-natural-iso.inv∘eta x = Nat-path λ _ → B.idl _
    ni .make-natural-iso.natural x y f =
      Nat-path λ _ → B.idr _ ∙ ap (B._∘ _) (y .F-id)

  pb .unitor-l {B = B} = to-natural-iso ni where
    module B = Cr B
    ni : make-natural-iso _ _
    ni .make-natural-iso.eta x = NT (λ _ → λ _ _ _ →
    ni .make-natural-iso.inv x = NT (λ _ → λ _ _ _ →
    ni .make-natural-iso.eta∘inv x = Nat-path λ _ → B.idl _
    ni .make-natural-iso.inv∘eta x = Nat-path λ _ → B.idl _
    ni .make-natural-iso.natural x y f = Nat-path λ _ → B.idr _ ∙

  pb .associator {A} {B} {C} {D} = to-natural-iso ni where
    module D = Cr D
    ni : make-natural-iso _ _
    ni .make-natural-iso.eta x = NT (λ _ → λ _ _ _ →
    ni .make-natural-iso.inv x = NT (λ _ → λ _ _ _ →
    ni .make-natural-iso.eta∘inv x = Nat-path λ _ → D.idl _
    ni .make-natural-iso.inv∘eta x = Nat-path λ _ → D.idl _
    ni .make-natural-iso.natural x y f = Nat-path λ _ →
      D.idr _ ·· D.pushl (y .fst .F-∘ _ _) ·· D.introl refl

  pb .triangle {C = C} f g = Nat-path (λ _ → Cr.idr C _)
  pb .pentagon {E = E} f g h i =
    Nat-path λ _ → ap₂ E._∘_
      (E.eliml (ap (f .F₁) (ap (g .F₁) (h .F-id)) ·· ap (f .F₁) (g .F-id) ·· f .F-id))
      (E.elimr (E.eliml (f .F-id)))
    where module E = Cr E

Lax functors🔗

In the same way that the definition of bicategory is obtained by starting with the definition of category and replacing the Hom\hom-sets by Hom\hom-categories (and adding coherence data to make sure the resulting structure is well-behaved), one can start with the definition of functor and replace the function between Hom\hom-sets by functors between Hom\hom-categories.

However, when talking about general bicategories, we are faced with a choice: We could generalise the functoriality axioms to natural isomorphisms, keeping with the fact that equations are invertible, but we could also drop this invertibility requirement, and work only with natural transformations P(idA)→idPAP(\id{id}_A) \to \id{id}_{PA}. When these are not invertible, the resulting structure is called a lax functor; When they are, we talk about pseudofunctors instead.

  Lax-functor (B : Prebicategory o ℓ ℓ′) (C : Prebicategory o₁ ℓ₁ ℓ₁′)
    : Type (o ⊔ o₁ ⊔ ℓ ⊔ ℓ₁ ⊔ ℓ′ ⊔ ℓ₁′) where

    module B = Prebicategory B
    module C = Prebicategory C

    P₀ : B.Ob → C.Ob
    P₁ : ∀ {A B} → Functor (B.Hom A B) (C.Hom (P₀ A) (P₀ B))

The resulting structure has “directed functoriality”, witnessed by the compositor and unitor natural transformations, which have components F1(f)F1(g)⇒F1(fg)F_1(f)F_1(g) \To F_1(fg) and F1(id)⇒idF_1(\id{id}) \To \id{id}.

      : ∀ {A B C}
      → C.compose F∘ Cat⟨ P₁ {B} {C} F∘ Fst , P₁ {A} {B} F∘ Snd ⟩Cat => P₁ F∘ B.compose

    unitor : ∀ {A} → C.⇒ P₁ .Functor.F₀ ( {A = A})

Additionally, we require the following three equations to hold, relating the compositor transformation to the associators, and the three unitors between themselves. We sketch the diagram which hexagon witnesses commutativity for, but leave the right-unit and left-unit diagrams undrawn (they’re boring commutative squares).

      : ∀ {a b c d} (f : c B.↦ d) (g : b B.↦ c) (h : a B.↦ b)
      → ₂ (B.α→ f g h) C.⊗ γ→ (f B.∘ g) h C.⊗ (γ→ f g C.◀ ₁ h)
      ≡ γ→ f (g B.∘ h) C.⊗ (₁ f C.▶ γ→ g h) C.⊗ C.α→ (₁ f) (₁ g) (₁ h)

      : ∀ {a b} (f : a B.↦ b)
      → ₂ (B.ρ← f) C.⊗ γ→ f C.⊗ (₁ f C.▶ unitor) ≡ C.ρ← (₁ f)

      : ∀ {a b} (f : a B.↦ b)
      → ₂ (B.λ← f) C.⊗ γ→ f C.⊗ (unitor C.◀ ₁ f) ≡ C.λ← (₁ f)


As mentioned above, a lax functor with invertible unitors and compositor is called a pseudofunctor. Every pseudofunctor has an underlying lax functor. Since invertibility is a property of 2-cells (rather than structure on 2-cells), “being pseudo” is a property of lax functors, not additional structure on lax functors.

  Pseudofunctor (B : Prebicategory o ℓ ℓ′) (C : Prebicategory o₁ ℓ₁ ℓ₁′)
    : Type (o ⊔ o₁ ⊔ ℓ ⊔ ℓ₁ ⊔ ℓ′ ⊔ ℓ₁′) where

    module B = Prebicategory B
    module C = Prebicategory C

    lax : Lax-functor B C

  open Lax-functor lax public

      : ∀ {a} → (unitor {a})
      : ∀ {a b c} (f : b B.↦ c) (g : a B.↦ b) → (γ→ f g)

  γ← : ∀ {a b c} (f : b B.↦ c) (g : a B.↦ b)
    → ₁ (f B.∘ g) C.⇒ ₁ f C.∘ ₁ g
  γ← f g = compositor-inv f g

  υ← : ∀ {a} → ₁ C.⇒
  υ← {a} = unitor-inv {a = a}

Lax transformations🔗

By dropping the invertibility requirement when generalising natural transformations to lax functors, we obtain the type of lax transformations between lax functors. If every 2-cell component of the lax transformation is invertible, we refer to it as a pseudonatural transformation. We omit the word “natural” in “lax natural transformation” for brevity.

The transformation which witnesses directed naturality for a lax transformation is called the naturator. In components, it witnesses commutativity of the diagram

and thus consists of a natural family of 2-cells G(f)σa⇒σbF(f)G(f)\sigma_a \To \sigma_bF(f).

  record Lax-transfor : Type (o ⊔ ℓ ⊔ ℓ₁ ⊔ ℓ′ ⊔ ℓ₁′) where
      σ : ∀ A → F.₀ A C.↦ G.₀ A
        : ∀ {a b}
        → preaction C (σ b) F∘ G.P₁ => postaction C (σ a) F∘ F.P₁

    ν→ : ∀ {a b} (f : a B.↦ b) → G.₁ f C.∘ σ a C.⇒ σ b C.∘ F.₁ f
    ν→ = naturator .η

The naturator ν\nu is required to be compatible with the compositor and unitor natural transformations of its source and target functors, which boil down to commutativity of the nightmarish diagrams in (Leinster 1998, sec. 1.2).

        : ∀ {a b c} (f : b B.↦ c) (g : a B.↦ b)
        → ν→ (f B.∘ g) C.⊗ (G.γ→ f g C.◀ σ a)
        ≡   (σ c C.▶ F.γ→ f g)
        C.⊗ C.α→ (σ c) (F.₁ f) (F.₁ g)
        C.⊗ (ν→ f C.◀ F.₁ g)
        C.⊗ C.α← (G.₁ f) (σ b) (F.₁ g)
        C.⊗ (G.₁ f C.▶ ν→ g)
        C.⊗ C.α→ (G.₁ f) (G.₁ g) (σ a)

        : ∀ {a}
        → ν→ ( {a}) C.⊗ (G.unitor C.◀ σ a)
        ≡ (σ a C.▶ F.unitor) C.⊗ C.ρ→ (σ a) C.⊗ C.λ← (σ a)

A lax transformation with invertible naturator is called a pseudonatural transformation.

  record Pseudonatural : Type (o ⊔ ℓ ⊔ ℓ₁ ⊔ ℓ′ ⊔ ℓ₁′) where
      lax : Lax-transfor

    open Lax-transfor lax public

      naturator-inv : ∀ {a b} (f : a B.↦ b) → (ν→ f)

    ν← : ∀ {a b} (f : a B.↦ b) → σ b C.∘ F.₁ f C.⇒ G.₁ f C.∘ σ a
    ν← f = naturator-inv f

We abbreviate the types of lax- and pseudonatural transformations by _=>ₗ_ and _=>ₚ_, respectively.

  _=>ₗ_ = Lax-transfor
  _=>ₚ_ = Pseudonatural


When dealing with 1-categorical data (categories, functors, and natural transformations), the commutativity in 2-cells is witnessed by equations in a set, which are trivial. When talking about bicategorical data, however, the naturality of a lax transformation is witnessed by a family of non-trivial 2-cells. Therefore, it is fruitful to consider transformations which affect this data: a natural family of 2-cells. This is called a modification between lax (or pseudo) transformations. Since we are directly dealing with sets (the sets of 2-cells), modifications are the simplest bicategorical widget to define.

  record Modification : Type (o ⊔ ℓ ⊔ ℓ₁′) where
      Γ : ∀ a → σ.σ a C.⇒ σ′.σ a

        : ∀ {a b} {f : a B.↦ b}
        → σ′.ν→ f C.⊗ (G.₁ f C.▶ Γ a)
        ≡ (Γ b C.◀ F.₁ f) C.⊗ σ.ν→ f

In a diagram, we display a modification as a 3-cell, i.e., a morphism (modification) between morphisms (lax transformations) between morphisms (lax functors) between objects (bicategories), and accordingly draw them with super-heavy arrows, as in the diagram below. Fortunately we will not often stumble onto diagrams of bicategories, rather studying diagrams in bicategories, which are (mercifully) limited to 2-cells.