🔍

Equations Inline Footnotes

open import Cat.Bi.Functor.Transformation
open import Cat.Bi.Solver
open import Cat.Bi.Base
open import Cat.Prelude

import Cat.Bi.Reasoning as Br

module Cat.Bi.Functor.Modification
  {o h l o' h' l'} {B : Prebicategory o h l} {C : Prebicategory o' h' l'}
  where

Identity and composition of modifications🔗

In analogy with how functors between categories $\mathcal{C}$ and $\mathcal{D}$ and together with natural transformations form the functor category $[\mathcal{C},\mathcal{D}]\text{,}$ lax functors between bicategories $\mathbf{B}$ and $\mathbf{C}$ similarly form a bicategory $[\mathbf{C},\mathbf{D}]$ where 0-cells are lax functors and 1-cells are lax transformations.

The 2-cells in this bicategory, that is, morphisms between lax transformations, are given by modifications. Here, we describe how modifications can be composed both vertically and horizontally, similarly to natural transformations between functors. In fact, these constructions very much resemble the corresponding constructions on natural transformations, so we won’t dwell too much on the details.

open Prebicategory C
open Modification
open _=>ₗ_

private
  module B  = Prebicategory B
  module C  = Br C
  module CH = C.Hom

module _ {F G : Lax-functor B C} where
  private
    module F = Lax-functor F
    module G = Lax-functor G

The identity modification has identity components.

  idmd : {α : F =>ₗ G} → Modification α α
  idmd .Γ _        = Hom.id
  idmd .is-natural = C.▶.elimr refl ∙ C.◀.introl refl

The vertical composition of two modifications between lax transformations is given by the componentwise composition.

  _∘md_ : {α β γ : F =>ₗ G} → Modification β γ → Modification α β → Modification α γ
  _∘md_ f g .Γ a                                    = f .Γ a ∘ g .Γ a
  _∘md_ {x} {y} {z} f g .is-natural {a} {b} {f = h} =
    ν→ z h ∘ G.₁ h ▶ (f .Γ a ∘ g .Γ a)       ≡⟨ CH.refl⟩∘⟨ C.▶-distribr ⟩≡
    ν→ z h ∘ G.₁ h ▶ f .Γ a ∘ G.₁ h ▶ g .Γ a ≡⟨ CH.extendl $ f .is-natural ⟩≡
    f .Γ b ◀ F.₁ h ∘ ν→ y h ∘ G.₁ h ▶ g .Γ a ≡⟨ CH.refl⟩∘⟨ g .is-natural ⟩≡
    f .Γ b ◀ F.₁ h ∘ g .Γ b ◀ F.₁ h ∘ ν→ x h ≡⟨ CH.pulll $ sym C.◀-distribl ⟩≡
    (f .Γ b ∘ g .Γ b) ◀ F.₁ h ∘ ν→ x h       ∎

module _ {F G H : Lax-functor B C} {α α' : G =>ₗ H} {β β' : F =>ₗ G} where
  private
    module F  = Lax-functor F
    module G  = Lax-functor G
    module H  = Lax-functor H
    module α  = _=>ₗ_ α
    module α' = _=>ₗ_ α'
    module β  = _=>ₗ_ β
    module β' = _=>ₗ_ β'

We proceed to describe the horizontal composition of modifications. Here we must give a modification from the composite $\alpha \beta$ to the composite ${\alpha }^{\prime }{\beta }^{\prime }\text{,}$ where $\alpha \text{,}$ ${\alpha }^{\prime }\text{,}$ $\beta \text{,}$ and ${\beta }^{\prime }$ are lax transformations, given a modification from $\alpha$ to ${\alpha }^{\prime }$ and one from $\beta$ to ${\beta }^{\prime }\text{.}$ Recalling that the composition $\alpha \beta$ is given by the componentwise composition $(\alpha \beta {)}_a={\alpha }_a{\beta }_a\text{,}$ we can use the horizontal composition native to the target bicategory to construct our composite modification.

  _◆md_ : Modification α α' → Modification β β' → Modification (α ∘lx β) (α' ∘lx β')
  (f ◆md g) .Γ x = f .Γ x C.◆ g .Γ x

  (f ◆md g) .is-natural {a} {b} {x} =
        (C.α← _ C.∘ α'.σ b C.▶ β'.ν→ x C.∘ C.α→ _ C.∘ α'.ν→ x C.◀ β'.σ a C.∘ C.α← _)
    C.∘ H.₁ x C.▶ (f .Γ a C.◆ g .Γ a)
      ≡⟨ bicat! C ⟩≡
        C.α← _ C.∘ α'.σ b C.▶ β'.ν→ x C.∘ C.α→ _ C.∘ ⌜ α'.ν→ x C.∘ H.₁ x C.▶ f .Γ a ⌝ C.◀ β'.σ a
    C.∘ C.α← _ C.∘ H.₁ x C.▶ (α.σ a C.▶ g .Γ a)
      ≡⟨ ap! (f .is-natural) ⟩≡
        C.α← _ C.∘ α'.σ b C.▶ β'.ν→ x C.∘ C.α→ _ C.∘ (f .Γ b C.◀ G.₁ x C.∘ α.ν→ x) C.◀ β'.σ a
    C.∘ C.α← _ C.∘ H.₁ x C.▶ (α.σ a C.▶ g .Γ a)
      ≡⟨ bicat! C ⟩≡
        C.α← _ C.∘ f .Γ b C.◀ (β'.σ b C.⊗ F.₁ x)
    C.∘ α.σ b C.▶ ⌜ β'.ν→ x C.∘ G.₁ x C.▶ g .Γ a ⌝ C.∘ C.α→ _ C.∘ α.ν→ x C.◀ β.σ a C.∘ C.α← _
      ≡⟨ ap! (g .is-natural) ⟩≡
        C.α← _ C.∘ f .Γ b C.◀ (β'.σ b C.⊗ F.₁ x)
    C.∘ α.σ b C.▶ (g .Γ b C.◀ F.₁ x C.∘ β.ν→ x) C.∘ C.α→ _ C.∘ α.ν→ x C.◀ β.σ a C.∘ C.α← _
      ≡⟨ bicat! C ⟩≡
        (f .Γ b C.◆ g .Γ b) C.◀ F.₁ x C.∘ C.α← _ C.∘ α.σ b C.▶ β.ν→ x C.∘ C.α→ _
    C.∘ α.ν→ x C.◀ β.σ a C.∘ C.α← _
      ∎