open import Cat.Functor.Naturality
open import Cat.Functor.Bifunctor
open import Cat.Instances.Product
open import Cat.Functor.Base
open import Cat.Bi.Base
open import Cat.Prelude

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

module Cat.Bi.Functor.Base where

Identity and composition for lax functors and pseudofunctorsπŸ”—

Having defined lax functors and pseudofunctors between bicategories, we should expect to be able to compose them, in analogy with ordinary functors between categories. This is indeed the case, and while the construction is unsurprising, showing the required coherence identities is a bit of an exercise.

private variable
  o1 o2 o3 h1 h2 h3 l1 l2 l3 : Level

open _=>_

module Lf-reasoning
  {B : Prebicategory o1 h1 l1} {C : Prebicategory o2 h2 l2}
  (F : Lax-functor B C) where

  private
    module B          = Prebicategory B
    module C          = Prebicategory C
    module CH {A} {B} = Cr (C.Hom A B)

  module P₁ {A} {B} = Fr (Lax-functor.P₁ F {A} {B})

  open Lax-functor F hiding (module P₁) public

  β–Ά-comp
    : βˆ€ {X Y Z} {f : Y B.↦ Z}
    β†’ postaction C (₁ f) F∘ P₁ {X} {Y} => P₁ F∘ postaction B f
  β–Ά-comp .Ξ· x              = Ξ³β†’ (_ , x)
  β–Ά-comp .is-natural x y Ξ± =
       CH.cdr (Fr.introl (preaction C (₁ y)) P₁.F-id) βˆ™βˆ™ Ξ³β†’nat _ _
    βˆ™βˆ™ CH.car (P₁.F-∘ _ _ βˆ™ CH.eliml (Fr.elim P₁ B.compose.β—€.F-id))

  β—€-comp
    : βˆ€ {X Y Z} {f : X B.↦ Y}
    β†’ preaction C (₁ f) F∘ P₁ {Y} {Z} => P₁ F∘ preaction B f
  β—€-comp .Ξ· x              = Ξ³β†’ (x , _)
  β—€-comp .is-natural x y Ξ± =
       CH.cdr (Fr.intror (postaction C (₁ x)) P₁.F-id) βˆ™βˆ™ Ξ³β†’nat _ _
    βˆ™βˆ™ CH.car (P₁.F-∘ _ _ βˆ™ CH.elimr (Fr.elim P₁ B.compose.β–Ά.F-id))

module Pf-reasoning
  {B : Prebicategory o1 h1 l1} {C : Prebicategory o2 h2 l2}
  (F : Pseudofunctor B C) where

  private
    module B          = Prebicategory B
    module C          = Prebicategory C
    module CH {A} {B} = Cr (C.Hom A B)

  module P₁ {A} {B} = Fr (Pseudofunctor.P₁ F {A} {B})

  open Pseudofunctor F hiding (module P₁) public

  open make-natural-iso
  open Cr.Inverses
  open Cr._β‰…_

  Ο…β‰… : βˆ€ {A} β†’ C.id CH.β‰… ₁ (B.id {A})
  Ο…β‰… .to       = Ο…β†’
  Ο…β‰… .from     = υ←
  Ο…β‰… .inverses = Cr.is-invertible.inverses unitor-inv

  compositor-ni
    : βˆ€ {A B C}
    β†’ Uncurry C.compose F∘ (P₁ {B} {C} FΓ— P₁ {A} {B}) ≅ⁿ P₁ F∘ Uncurry B.compose
  compositor-ni = to-natural-iso ni where
    ni : make-natural-iso _ _
    ni .eta       = Ξ³β†’
    ni .inv       = γ←
    ni .eta∘inv _ = Cr.is-invertible.inverses (compositor-inv _) .invl
    ni .inv∘eta _ = Cr.is-invertible.inverses (compositor-inv _) .invr
    ni .make-natural-iso.natural _ _ _ = sym $ Ξ³β†’nat _ _

  Ξ³β‰… : βˆ€ {A B C} {f : B B.↦ C} {g : A B.↦ B} β†’ ₁ f C.βŠ— ₁ g CH.β‰… ₁ (f B.βŠ— g)
  Ξ³β‰… = isoⁿ→iso compositor-ni _

  β–Ά-comp
    : βˆ€ {X Y Z} {f : Y B.↦ Z}
    β†’ postaction C (₁ f) F∘ P₁ {X} {Y} ≅ⁿ P₁ F∘ postaction B f
  β–Ά-comp = to-natural-iso ni where
    ni : make-natural-iso _ _
    ni .eta x     = Ξ³β†’ (_ , x)
    ni .inv x     = γ← (_ , x)
    ni .eta∘inv _ = Cr.is-invertible.inverses (compositor-inv _) .invl
    ni .inv∘eta _ = Cr.is-invertible.inverses (compositor-inv _) .invr
    ni .natural x y Ξ± = sym
       $ CH.cdr (Fr.introl (preaction C (₁ y)) P₁.F-id) βˆ™βˆ™ Ξ³β†’nat _ _
      βˆ™βˆ™ CH.car (P₁.F-∘ _ _ βˆ™ CH.eliml (Fr.elim P₁ B.compose.β—€.F-id))

  β—€-comp
    : βˆ€ {X Y Z} {f : X B.↦ Y}
    β†’ preaction C (₁ f) F∘ P₁ {Y} {Z} ≅ⁿ P₁ F∘ preaction B f
  β—€-comp = to-natural-iso ni where
    ni : make-natural-iso _ _
    ni .eta x     = Ξ³β†’ (x , _)
    ni .inv x     = γ← (x , _)
    ni .eta∘inv _ = Cr.is-invertible.inverses (compositor-inv _) .invl
    ni .inv∘eta _ = Cr.is-invertible.inverses (compositor-inv _) .invr
    ni .natural x y Ξ± = sym
       $ CH.cdr (Fr.intror (postaction C (₁ x)) P₁.F-id) βˆ™βˆ™ Ξ³β†’nat _ _
      βˆ™βˆ™ CH.car (P₁.F-∘ _ _ βˆ™ CH.elimr (Fr.elim P₁ B.compose.β–Ά.F-id))

open Pseudofunctor
open Lax-functor

module _ {B : Prebicategory o1 h1 l1} where
  open Br B

The identity lax functor on a bicategory is constructed from the identity function on objects, and the identity functor on 

  IdL : Lax-functor B B
  IdL .Pβ‚€ z = z
  IdL .P₁   = Id

For the compositor and unitor, we can also choose the identity; the coherence conditions work out to be trivial.

  IdL .compositor .Ξ· x              = Hom.id
  IdL .compositor .is-natural _ _ _ = Hom.id-comm-sym
  IdL .unitor                       = Hom.id

  IdL .hexagon f g h =
    Hom.elimr (Hom.idl _ βˆ™ β—€.F-id) βˆ™ Hom.insertl (Hom.idl _ βˆ™ β–Ά.F-id)
  IdL .right-unit f = Hom.elimr (Hom.idl _ βˆ™ β–Ά.F-id)
  IdL .left-unit f  = Hom.elimr (Hom.idl _ βˆ™ β—€.F-id)

Since identity morphisms are invertible, this extends directly to a pseudofunctor as well.

  IdP : Pseudofunctor B B
  IdP .lax              = IdL
  IdP .unitor-inv       = Hom.id-invertible
  IdP .compositor-inv _ = Hom.id-invertible

module _
  {B : Prebicategory o1 h1 l1} {C : Prebicategory o2 h2 l2}
  {D : Prebicategory o3 h3 l3}
  where
  private
    module B  = Prebicategory B
    module C  = Prebicategory C
    module D  = Br D
    module DH = D.Hom
    module Pr = Pf-reasoning

It is similarly straightforward to define the composite of two lax functors and by composing the object functions and 1-cell functors.

  _L∘_ : Lax-functor C D β†’ Lax-functor B C β†’ Lax-functor B D
  F L∘ G = lf module L∘ where

    private
      module F = Lf-reasoning F
      module G = Lax-functor G
    lf : Lax-functor _ _

    lf .Pβ‚€ = F.Pβ‚€ βŠ™ G.Pβ‚€
    lf .P₁ = F.P₁ F∘ G.P₁

For the compositor of the composite functor, we must construct a 2-cell Using the compositor of we have and mapping the compositor of under in the result, we get the required morphism. Naturality of this construction amounts to applying the naturality of the original compositors in turn.

    lf .compositor .Ξ· (x , y) = F.β‚‚ (G.Ξ³β†’ (x , y)) D.∘ F.Ξ³β†’ (G.₁ x , G.₁ y)
    lf .compositor .is-natural (x , y) (x' , y') (f , g) =
      (F.β‚‚ (G.Ξ³β†’ _) D.∘ F.Ξ³β†’ _) D.∘ (F.β‚‚ (G.β‚‚ f) D.β—† F.β‚‚ (G.β‚‚ g)) β‰‘βŸ¨ DH.extendr (F.Ξ³β†’nat (G.β‚‚ f) (G.β‚‚ g)) βŸ©β‰‘
      (F.β‚‚ (G.Ξ³β†’ _) D.∘ F.β‚‚ (G.β‚‚ f C.β—† G.β‚‚ g)) D.∘ F.Ξ³β†’ _         β‰‘βŸ¨ DH.pushl (F.P₁.weave (G.Ξ³β†’nat f g)) βŸ©β‰‘
      F.β‚‚ (G.β‚‚ (f B.β—† g)) D.∘ F.β‚‚ (G.Ξ³β†’ _) D.∘ F.Ξ³β†’ _             ∎

The unitor follows a similar pattern.

    lf .unitor = F.β‚‚ G.Ο…β†’ D.∘ F.Ο…β†’

Showing that the coherence equations hold for these constructions is in principle a straightforward matter of applying of the identities for and in sequence, but the sheer size of the equations make it a bit daunting. We show the case for the left unit to illustrate the point, but elide the other two equations which are similar in spirit.

    lf .left-unit f =
          F.β‚‚ (G.β‚‚ (B.λ← f)) D.∘ (F.β‚‚ (G.Ξ³β†’ (B.id , f)) D.∘ F.Ξ³β†’ (G.₁ B.id , G.₁ f))
      D.∘ (F.β‚‚ G.Ο…β†’ D.∘ F.Ο…β†’) D.β—€ F.₁ (G.₁ f)
        β‰‘Λ˜βŸ¨ DH.refl⟩∘⟨ DH.pushr (DH.extendl (sym $ F.β—€-comp .is-natural _ _ _) βˆ™ ap (F.Ξ³β†’ _ D.∘_) (sym D.β—€-distribl)) βŸ©β‰‘Λ˜
          F.β‚‚ (G.β‚‚ (B.λ← f)) D.∘ F.β‚‚ (G.Ξ³β†’ (B.id , f)) D.∘ F.β‚‚ (G.Ο…β†’ C.β—€ G.₁ f)
      D.∘ F.Ξ³β†’ (C.id , G.₁ f) D.∘ F.Ο…β†’ D.β—€ F.₁ (G.₁ f)
        β‰‘βŸ¨ F.P₁.pulll3 (G.left-unit f) βŸ©β‰‘
      F.β‚‚ (C.λ← (G.₁ f)) D.∘ F.Ξ³β†’ (C.id , G.₁ f) D.∘ F.Ο…β†’ D.β—€ F.₁ (G.₁ f)
        β‰‘βŸ¨ F.left-unit (G.₁ f) βŸ©β‰‘
      D.λ← (F.₁ (G.₁ f))
        ∎
Here are the hexagon and right unit identities, not for the faint of heart. 
    lf .hexagon f g h =
          F.β‚‚ (G.β‚‚ (B.Ξ±β†’ _)) D.∘ (F.β‚‚ (G.Ξ³β†’ _) D.∘ F.Ξ³β†’ _)
      D.∘ (F.β‚‚ (G.Ξ³β†’ _) D.∘ F.Ξ³β†’ _) D.β—€ F.₁ (G.₁ h)
        β‰‘Λ˜βŸ¨ DH.refl⟩∘⟨ DH.pushr (DH.extendl (sym $ F.β—€-comp .is-natural _ _ _) βˆ™ ap (F.Ξ³β†’ _ D.∘_) (sym D.β—€-distribl)) βŸ©β‰‘Λ˜
          F.β‚‚ (G.β‚‚ (B.Ξ±β†’ _)) D.∘ F.β‚‚ (G.Ξ³β†’ _) D.∘ F.β‚‚ (G.Ξ³β†’ _ C.β—€ G.₁ h) D.∘ F.Ξ³β†’ _
      D.∘ F.Ξ³β†’ _ D.β—€ F.₁ (G.₁ h)
        β‰‘βŸ¨ F.P₁.extendl3 (G.hexagon f g h) βŸ©β‰‘
          F.β‚‚ (G.Ξ³β†’ _) D.∘ F.β‚‚ (G.₁ f C.β–Ά G.Ξ³β†’ _) D.∘ F.β‚‚ (C.Ξ±β†’ _)
      D.∘ F.Ξ³β†’ _ D.∘ F.Ξ³β†’ _ D.β—€ F.₁ (G.₁ h)
        β‰‘βŸ¨ DH.refl⟩∘⟨ DH.refl⟩∘⟨ F.hexagon (G.₁ f) (G.₁ g) (G.₁ h) βŸ©β‰‘
          F.β‚‚ (G.Ξ³β†’ _) D.∘ F.β‚‚ (G.₁ f C.β–Ά G.Ξ³β†’ _) D.∘ F.Ξ³β†’ _
      D.∘ F.₁ (G.₁ f) D.β–Ά F.Ξ³β†’ _ D.∘ D.Ξ±β†’ _
        β‰‘βŸ¨ DH.refl⟩∘⟨ DH.extendl (sym $ F.β–Ά-comp .is-natural _ _ _) βŸ©β‰‘
          F.β‚‚ (G.Ξ³β†’ _) D.∘ F.Ξ³β†’ _ D.∘ F.₁ (G.₁ f) D.β–Ά F.β‚‚ (G.Ξ³β†’ _)
      D.∘ F.₁ (G.₁ f) D.β–Ά F.Ξ³β†’ _ D.∘ D.Ξ±β†’ _
        β‰‘βŸ¨ DH.pushr (ap (F.Ξ³β†’ _ D.∘_) (D.β–Ά.pulll refl)) βŸ©β‰‘
          (F.β‚‚ (G.Ξ³β†’ (f , g B.βŠ— h)) D.∘ F.Ξ³β†’ (G.₁ f , G.₁ (g B.βŠ— h)))
      D.∘ F.₁ (G.₁ f) D.β–Ά (F.β‚‚ (G.Ξ³β†’ (g , h)) D.∘ F.Ξ³β†’ (G.₁ g , G.₁ h)) D.∘ D.Ξ±β†’ _
        ∎
    lf .right-unit f =
          F.β‚‚ (G.β‚‚ (B.ρ← f)) D.∘ (F.β‚‚ (G.Ξ³β†’ (f , B.id)) D.∘ F.Ξ³β†’ (G.₁ f , G.₁ B.id))
      D.∘ F.₁ (G.₁ f) D.β–Ά (F.β‚‚ G.Ο…β†’ D.∘ F.Ο…β†’)
        β‰‘Λ˜βŸ¨ DH.refl⟩∘⟨ DH.pushr (DH.extendl (sym $ F.β–Ά-comp .is-natural _ _ _) βˆ™ ap (F.Ξ³β†’ _ D.∘_) (sym D.β–Ά-distribr)) βŸ©β‰‘Λ˜
          F.β‚‚ (G.β‚‚ (B.ρ← f)) D.∘ F.β‚‚ (G.Ξ³β†’ (f , B.id)) D.∘ F.β‚‚ (G.₁ f C.β–Ά G.Ο…β†’)
      D.∘ F.Ξ³β†’ (G.₁ f , C.id) D.∘ F.₁ (G.₁ f) D.β–Ά F.Ο…β†’
        β‰‘βŸ¨ F.P₁.pulll3 (G.right-unit f) βŸ©β‰‘
      F.β‚‚ (C.ρ← (G.₁ f)) D.∘ F.Ξ³β†’ (G.₁ f , C.id) D.∘ F.₁ (G.₁ f) D.β–Ά F.Ο…β†’
        β‰‘βŸ¨ F.right-unit (G.₁ f) βŸ©β‰‘
      D.ρ← (F.₁ (G.₁ f))
        ∎

Finally, pseudofunctors can be composed using the same construction, thanks to the fact that functors preserve isomorphisms.

  _P∘_ : Pseudofunctor C D β†’ Pseudofunctor B C β†’ Pseudofunctor B D
  (F P∘ G) .lax        = F .lax L∘ G .lax
  (F P∘ G) .unitor-inv = DH.invertible-∘
    (Pr.P₁.F-map-invertible F (Pr.unitor-inv G)) (Pr.unitor-inv F)
  (F P∘ G) .compositor-inv _ = DH.invertible-∘
    (Pr.P₁.F-map-invertible F (Pr.compositor-inv G _)) (Pr.compositor-inv F _)

{-# DISPLAY L∘.lf F G = F L∘ G #-}