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 sets, a prebicategory has 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 and for each a precategory We refer to the type of objects of by and call its inhabitants maps or 1-cells; In the second dimension, between each pair of maps we have a set of 2-cells (sometimes homotopies), written

The composition operation of called vertical composition, will be written 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 with 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 30 _∘_
  infixr 25 _βŠ—_
  infix 35 _β—€_ _β–Ά_

  -- 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.Β  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 to the right unitor as and to the associator as 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: 

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 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 evaporates, leaving only 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 by (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 by functors between

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 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 and 

    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 

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

References