open import Cat.Functor.Naturality
open import Cat.Instances.Product
open import Cat.Functor.Compose renaming (_◆_ to _◇_)
open import Cat.Functor.Base
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

Prebicategories🔗

open _=>_

module _ where
  open Functor
  compose-assocˡ
    : ∀ {o ℓ ℓ'} {O : Type o} {H : O → O → Precategory ℓ ℓ'}
    → (C : ∀ {A B C} → Functor (H B C ×ᶜ H A B) (H A C))
    → ∀ {A B C D}
    → Functor (H C D ×ᶜ H B C ×ᶜ H A B) (H A D)
  compose-assocˡ C .F₀ (F , G , H) = C .F₀ (C .F₀ (F , G) , H)
  compose-assocˡ C .F₁ (f , g , h) = C .F₁ (C .F₁ (f , g) , h)
  compose-assocˡ C .F-id = ap (C .F₁) (Σ-pathp (C .F-id) refl) ∙ C .F-id
  compose-assocˡ C .F-∘ f g = ap (C .F₁) (Σ-pathp (C .F-∘ _ _) refl) ∙ C .F-∘ _ _

  compose-assocʳ
    : ∀ {o ℓ ℓ'} {O : Type o} {H : O → O → Precategory ℓ ℓ'}
    → (C : ∀ {A B C} → Functor (H B C ×ᶜ H A B) (H A C))
    → ∀ {A B C D}
    → Functor (H C D ×ᶜ H B C ×ᶜ H A B) (H A D)
  compose-assocʳ C .F₀ (F , G , H) = C .F₀ (F , C .F₀ (G , H))
  compose-assocʳ C .F₁ (f , g , h) = C .F₁ (f , C .F₁ (g , h))
  compose-assocʳ C .F-id = ap (C .F₁) (Σ-pathp refl (C .F-id)) ∙ C .F-id
  compose-assocʳ C .F-∘ f g = ap (C .F₁) (Σ-pathp refl (C .F-∘ _ _)) ∙ C .F-∘ _ _

private variable o ℓ ℓ' o₁ ℓ₁ ℓ₁' : Level

A (pre)bicategory is the natural higher-dimensional generalisation of a (pre)category. Whereas a precategory has $\mathbf{Hom}\text{-}$sets, a prebicategory has $\mathbf{Hom}\text{-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 $\mathbf{Ob}\text{,}$ and for each $A,B:\mathbf{Ob}\text{,}$ a precategory $\mathbf{Hom}(A,B)\text{.}$ We refer to the type of objects of $\mathbf{Hom}(A,B)$ by $A\mapsto B\text{,}$ and call its inhabitants maps or 1-cells; In the second dimension, between each pair of maps $f,g\text{,}$ we have a set of 2-cells (sometimes homotopies), written $f\Rightarrow g\text{.}$

The composition operation of $\mathbf{Hom}(A,B)\text{,}$ called vertical composition, will be written $\alpha \otimes \beta \text{.}$ As for why it’s called vertical composition, note that it reduces pasting diagrams of the form

record Prebicategory o ℓ ℓ' : Type (lsuc (o ⊔ ℓ ⊔ ℓ')) where
  no-eta-equality
  field
    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 $\mathbf{Hom}\text{-sets}$ with $\mathbf{Hom}\text{-precategories,}$ we should replace our maps of sets for maps of precategories, i.e., functors.

  field
    id      : ∀ {A} → ⌞ Hom A A ⌟
    compose : ∀ {A B C} → Functor (Hom B C ×ᶜ Hom A B) (Hom A C)

  module compose {a} {b} {c} = Fr (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 = ⌞ 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 # (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  _∘_
  infixr  _⊗_
  infix  _◀_ _▶_

  -- 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₁ (Hom.id , 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 , Hom.id)

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. $(\mathrm{id}\circ -)\cong \mathrm{id}\text{,}$ which witnesses that the functor “compose with the identity 1-cell on the left” is naturally isomorphic to the identity functor.

  field
    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)

    associator
      : ∀ {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 \text{,}$ to the right unitor as $\rho \text{,}$ and to the associator as $\alpha \text{,}$ 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._≅_.to .η

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

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

  ρ←nat : ∀ {A B} {f f' : A ↦ B} (β : f ⇒ f')
        → Path ((f ⊗ id) ⇒ f') (ρ← _ ∘ (β ◀ id)) (β ∘ ρ← _)
  ρ←nat {A} {B} {f} {f'} β = unitor-r .Cr.from .is-natural f f' β

  λ←nat : ∀ {A B} {f f' : A ↦ B} (β : f ⇒ f')
        → Path ((id ⊗ f) ⇒ f') (λ← _ ∘ (id ▶ β)) (β ∘ λ← _)
  λ←nat {A} {B} {f} {f'} β = unitor-l .Cr.from .is-natural f f' β

  ρ→nat : ∀ {A B} {f f' : A ↦ B} (β : f ⇒ f')
        → Path (f ⇒ f' ⊗ id) (ρ→ _ ∘ β) ((β ◀ id) ∘ ρ→ _)
  ρ→nat {A} {B} {f} {f'} β = unitor-r .Cr.to .is-natural f f' β

  λ→nat : ∀ {A B} {f f' : A ↦ B} (β : f ⇒ f')
        → Path (f ⇒ id ⊗ f') (λ→ _ ∘ β) ((id ▶ β) ∘ λ→ _)
  λ→nat {A} {B} {f} {f'} β = unitor-l .Cr.to .is-natural f f' β

  α→ : ∀ {A B C D} (f : C ↦ D) (g : B ↦ C) (h : A ↦ B)
     → (f ⊗ g) ⊗ h ⇒ f ⊗ (g ⊗ h)
  α→ f g h = associator .Cr._≅_.to .η (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)

  α←nat : ∀ {A B C D} {f f' : C ↦ D} {g g' : B ↦ C} {h h' : A ↦ B}
        → (β : f ⇒ f') (γ : g ⇒ g') (δ : h ⇒ h')
        → Path (f ⊗ g ⊗ h ⇒ ((f' ⊗ g') ⊗ h'))
          (α← _ _ _ ∘ (β ◆ (γ ◆ δ))) (((β ◆ γ) ◆ δ) ∘ α← _ _ _)
  α←nat {A} {B} {C} {D} {f} {f'} {g} {g'} {h} {h'} β γ δ =
    associator .Cr._≅_.from .is-natural (f , g , h) (f' , g' , h') (β , γ , δ)

  α→nat : ∀ {A B C D} {f f' : C ↦ D} {g g' : B ↦ C} {h h' : A ↦ B}
        → (β : f ⇒ f') (γ : g ⇒ g') (δ : h ⇒ h')
        → Path ((f ⊗ g) ⊗ h ⇒ (f' ⊗ g' ⊗ h'))
           (α→ _ _ _ ∘ ((β ◆ γ) ◆ δ))
           ((β ◆ (γ ◆ δ)) ∘ α→ _ _ _)
  α→nat {A} {B} {C} {D} {f} {f'} {g} {g'} {h} {h'} β γ δ =
    associator .Cr._≅_.to .is-natural (f , g , h) (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

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

    pentagon
      : ∀ {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: $\mathbf{B}\text{,}$ $\mathbf{C}\text{.}$

module _ (B : Prebicategory o ℓ ℓ') where
  open Prebicategory B
  open Functor

  postaction : ∀ {a b c} (f : a ↦ b) → Functor (Hom c a) (Hom c b)
  postaction f .F₀ g = f ⊗ g
  postaction f .F₁ g = f ▶ g
  postaction f .F-id = compose.F-id
  postaction f .F-∘ g h =
    f ▶ (g ∘ h)                 ≡˘⟨ ap (_◆ g ∘ h) (Hom.idl Hom.id) ⟩≡˘
    (Hom.id ∘ Hom.id) ◆ (g ∘ h) ≡⟨ compose.F-∘ _ _ ⟩≡
    (f ▶ g) ∘ (f ▶ h)           ∎

  preaction : ∀ {a b c} (f : a ↦ b) → Functor (Hom b c) (Hom a c)
  preaction f .F₀ g = g ⊗ f
  preaction f .F₁ g = g ◀ f
  preaction f .F-id = compose.F-id
  preaction f .F-∘ g h =
    (g ∘ h) ◀ f                 ≡˘⟨ ap (g ∘ h ◆_) (Hom.idl Hom.id) ⟩≡˘
    (g ∘ h) ◆ (Hom.id ∘ Hom.id) ≡⟨ compose.F-∘ _ _ ⟩≡
    (g ◀ f) ∘ (h ◀ f)           ∎

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.

{-# TERMINATING #-}
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 we have already done (but off-screen, since its construction is very straightforward).

  pb .compose = F∘-functor

The unitors and associator are almost, but not quite, given by the identity 2-cells, since componentwise the functor composition $\mathrm{id}\circ F$ evaporates, leaving only $F$ 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 {D = Cat[ _ , _ ]} _ _
    ni .make-natural-iso.eta x = NT (λ _ → B.id) λ _ _ _ → B.id-comm-sym
    ni .make-natural-iso.inv x = NT (λ _ → B.id) λ _ _ _ → B.id-comm-sym
    ni .make-natural-iso.eta∘inv x = ext λ _ → B.idl _
    ni .make-natural-iso.inv∘eta x = ext λ _ → B.idl _
    ni .make-natural-iso.natural x y f =
      ext λ _ → 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 {D = Cat[ _ , _ ]} _ _
    ni .make-natural-iso.eta x = NT (λ _ → B.id) λ _ _ _ → B.id-comm-sym
    ni .make-natural-iso.inv x = NT (λ _ → B.id) λ _ _ _ → B.id-comm-sym
    ni .make-natural-iso.eta∘inv x = ext λ _ → B.idl _
    ni .make-natural-iso.inv∘eta x = ext λ _ → B.idl _
    ni .make-natural-iso.natural x y f = ext λ _ → B.idr _ ∙ B.id-comm

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

  pb .triangle {C = C} f g = ext λ _ → Cr.idr C _
  pb .pentagon {E = E} f g h i = ext λ _ → 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 $\mathbf{Hom}\text{-sets}$ by $\mathbf{Hom}\text{-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 $\mathbf{Hom}\text{-sets}$ by functors between $\mathbf{Hom}\text{-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({\mathrm{id}}_A)\to {\mathrm{id}}_{PA}\text{.}$ When these are not invertible, the resulting structure is called a lax functor; When they are, we talk about pseudofunctors instead.

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

  private
    module B = Prebicategory B
    module C = Prebicategory C

  field
    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 $F_1(f)F_1(g)\Rightarrow F_1(fg)$ and $\mathrm{id}\Rightarrow F_1(\mathrm{id})\text{.}$

    compositor
      : ∀ {A B C}
      → C.compose F∘ (P₁ {B} {C} F× P₁ {A} {B}) => P₁ F∘ B.compose

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

  module P₁ {A} {B} = Functor (P₁ {A} {B})

  ₀ : B.Ob → C.Ob
  ₀ = P₀

  ₁ : ∀ {a b} → a B.↦ b → P₀ a C.↦ P₀ b
  ₁ = P₁.F₀

  ₂ : ∀ {a b} {f g : a B.↦ b} → f B.⇒ g → ₁ f C.⇒ ₁ g
  ₂ = P₁.F₁

  γ→ : ∀ {a b c} (f : b B.↦ c) (g : a B.↦ b)
     → ₁ f C.⊗ ₁ g C.⇒ ₁ (f B.⊗ g)
  γ→ f g = compositor .η (f , g)

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).

  field
    hexagon
      : ∀ {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)

    right-unit
      : ∀ {a b} (f : a B.↦ b)
      → ₂ (B.ρ← f) C.∘ γ→ f B.id C.∘ (₁ f C.▶ unitor) ≡ C.ρ← (₁ f)

    left-unit
      : ∀ {a b} (f : a B.↦ b)
      → ₂ (B.λ← f) C.∘ γ→ B.id f C.∘ (unitor C.◀ ₁ f) ≡ C.λ← (₁ f)

Pseudofunctors🔗

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.

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

  private
    module B = Prebicategory B
    module C = Prebicategory C

  field
    lax : Lax-functor B C

  open Lax-functor lax public

  field
    unitor-inv
      : ∀ {a} → C.Hom.is-invertible (unitor {a})
    compositor-inv
      : ∀ {a b c} (f : b B.↦ c) (g : a B.↦ b) → C.Hom.is-invertible (γ→ 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 .Cr.is-invertible.inv

  υ← : ∀ {a} → ₁ B.id C.⇒ C.id
  υ← {a} = unitor-inv {a = a} .Cr.is-invertible.inv

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.

module
  _ {B : Prebicategory o ℓ ℓ'} {C : Prebicategory o₁ ℓ₁ ℓ₁'}
    (F : Lax-functor B C) (G : Lax-functor B C)
  where
  private
    module B = Prebicategory B
    module C = Prebicategory C
    module F = Lax-functor F
    module G = Lax-functor G

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){\sigma }_a\Rightarrow {\sigma }_{b}F(f)\text{.}$

  record Lax-transfor : Type (o ⊔ ℓ ⊔ ℓ₁ ⊔ ℓ' ⊔ ℓ₁') where
    field
      σ : ∀ A → F.₀ A C.↦ G.₀ A
      naturator
        : ∀ {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).

    field
      ν-compositor
        : ∀ {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)

      ν-unitor
        : ∀ {a}
        → ν→ (B.id {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
    field
      lax : Lax-transfor

    open Lax-transfor lax public

    field
      naturator-inv : ∀ {a b} (f : a B.↦ b) → C.Hom.is-invertible (ν→ f)

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

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

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

Modifications🔗

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.

module
  _ {B : Prebicategory o ℓ ℓ'} {C : Prebicategory o₁ ℓ₁ ℓ₁'}
    {F : Lax-functor B C} {G : Lax-functor B C}
    (σ σ' : F =>ₗ G)
  where

  private
    module B = Prebicategory B
    module C = Prebicategory C
    module F = Lax-functor F
    module G = Lax-functor G
    module σ = Lax-transfor σ
    module σ' = Lax-transfor σ'

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

      is-natural
        : ∀ {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.