module Cat.Functor.Bifunctor
  {o₁ h₁ oβ‚‚ hβ‚‚ o₃ h₃ : _}
  {C : Precategory o₁ h₁}
  {D : Precategory oβ‚‚ hβ‚‚}
  {E : Precategory o₃ h₃}
  (F : Functor (C Γ—αΆœ D) E)
  where

BifunctorsπŸ”—

The word bifunctor is a term of endearment for β€œfunctors out of a product category”. They’re named after bilinear maps, to evoke the idea that a functor out of is functorial in each of its arguments. Correspondingly we have the operations first and second, altering one coordinate and leaving the other fixed.

first : βˆ€ {a b} {x} β†’ C.Hom a b β†’ E.Hom (Fβ‚€ (a , x)) (Fβ‚€ (b , x))
first f = F₁ (f , D.id)

second : βˆ€ {a b} {x} β†’ D.Hom a b β†’ E.Hom (Fβ‚€ (x , a)) (Fβ‚€ (x , b))
second f = F₁ (C.id , f)

These operations behave functorially by themselves, and you can β€œpush second past first”.

first-id : βˆ€ {a} {x} β†’ first C.id ≑ E.id {Fβ‚€ (x , a)}
first-id = F-id

second-id : βˆ€ {a} {x} β†’ second D.id ≑ E.id {Fβ‚€ (x , a)}
second-id = F-id

first∘first : βˆ€ {a b c} {x} {f : C.Hom b c} {g : C.Hom a b}
            β†’ first (f C.∘ g)
            ≑ first {x = x} f E.∘ first g
first∘first {f = f} {g} = sym (
  F₁ (f , D.id) E.∘ F₁ (g , D.id) β‰‘βŸ¨ sym (F-∘ _ _) βŸ©β‰‘
  F₁ (f C.∘ g , D.id D.∘ D.id)    β‰‘βŸ¨ ap (Ξ» e β†’ F₁ (f C.∘ g , e)) (D.idl _) βŸ©β‰‘
  F₁ (f C.∘ g , D.id)             ∎
  )

second∘second : βˆ€ {a b c} {x} {f : D.Hom b c} {g : D.Hom a b}
              β†’ second (f D.∘ g)
              ≑ second {x = x} f E.∘ second g
second∘second {f = f} {g} = sym (
  F₁ (C.id , f) E.∘ F₁ (C.id , g) β‰‘βŸ¨ sym (F-∘ _ _) βŸ©β‰‘
  F₁ (C.id C.∘ C.id , f D.∘ g)    β‰‘βŸ¨ ap (Ξ» e β†’ F₁ (e , f D.∘ g)) (C.idl _) βŸ©β‰‘
  F₁ (C.id , f D.∘ g)             ∎
  )

first∘second : βˆ€ {a b} {x y} {f : C.Hom a b} {g : D.Hom x y}
             β†’ first f E.∘ second g
             ≑ second g E.∘ first f
first∘second {f = f} {g} =
  F₁ (f , D.id) E.∘ F₁ (C.id , g) β‰‘βŸ¨ sym (F-∘ _ _) βŸ©β‰‘
  F₁ (f C.∘ C.id , D.id D.∘ g)    β‰‘βŸ¨ apβ‚‚ (Ξ» x y β†’ F₁ (x , y)) (C.idr _ βˆ™ sym (C.idl _)) (D.idl _ βˆ™ sym (D.idr _)) βŸ©β‰‘
  F₁ (C.id C.∘ f , g D.∘ D.id)    β‰‘βŸ¨ F-∘ _ _ βŸ©β‰‘
  F₁ (C.id , g) E.∘ F₁ (f , D.id) ∎

Fixing an object in either of the categories gives us a functor which varies in the other category.

Left : D.Ob β†’ Functor C E
Left y .Functor.Fβ‚€ x = Fβ‚€ (x , y)
Left y .Functor.F₁ f = first f
Left y .Functor.F-id = F-id
Left y .Functor.F-∘ f g = first∘first

Right : C.Ob β†’ Functor D E
Right x .Functor.Fβ‚€ y = Fβ‚€ (x , y)
Right x .Functor.F₁ f = second f
Right x .Functor.F-id = F-id
Right x .Functor.F-∘ f g = second∘second

Flip : Functor (D Γ—αΆœ C) E
Flip .Functor.Fβ‚€ (x , y) = Fβ‚€ (y , x)
Flip .Functor.F₁ (x , y) = F₁ (y , x)
Flip .Functor.F-id    = F-id
Flip .Functor.F-∘ f g = F-∘ _ _