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


# Prebicategories🔗

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

The composition operation of $\mathbf{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
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}$-sets with $\mathbf{Hom}$-precategories, we should replace our maps of sets for maps of precategories, i.e., functors.

  field
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} = 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 = 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 _⊗_
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. $(\mathrm{id}_{} \circ -) \mathrm{Id}$, 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$, 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._≅_.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 , 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}$, $\mathbf{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.

{-# 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 _ _
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 = 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 (λ _ → 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 = 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 _ ∙ B.id-comm

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 (λ _ → 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 = 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 $\mathbf{Hom}$-sets by $\mathbf{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 $\mathbf{Hom}$-sets by functors between $\mathbf{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(\mathrm{id}_{A}) \to \mathrm{id}_{PA}$. 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 $F_1(\mathrm{id}_{}) \Rightarrow \mathrm{id}_{}$.

    compositor
: ∀ {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.id C.⇒ P₁ .Functor.F₀ (B.id {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).  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.

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_bF(f)$.

  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 .

    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.

  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.  