open import Cat.Instances.Product
open import Cat.Prelude

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)


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 CΓ—CatD\ca{C} \times_\cat \ca{D} 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 ,

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

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

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

second-id : βˆ€ {a} {x} β†’ second ≑ {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 , E.∘ F₁ (g , β‰‘βŸ¨ sym (F-∘ _ _) βŸ©β‰‘
  F₁ (f C.∘ g , D.∘    β‰‘βŸ¨ ap (Ξ» e β†’ F₁ (f C.∘ g , e)) (D.idl _) βŸ©β‰‘
  F₁ (f C.∘ g ,             ∎

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₁ ( , f) E.∘ F₁ ( , g) β‰‘βŸ¨ sym (F-∘ _ _) βŸ©β‰‘
  F₁ ( C.∘ , f D.∘ g)    β‰‘βŸ¨ ap (Ξ» e β†’ F₁ (e , f D.∘ g)) (C.idl _) βŸ©β‰‘
  F₁ ( , 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 , E.∘ F₁ ( , g) β‰‘βŸ¨ sym (F-∘ _ _) βŸ©β‰‘
  F₁ (f C.∘ , D.∘ g)    β‰‘βŸ¨ apβ‚‚ (Ξ» x y β†’ F₁ (x , y)) (C.idr _ βˆ™ sym (C.idl _)) (D.idl _ βˆ™ sym (D.idr _)) βŸ©β‰‘
  F₁ ( C.∘ f , g D.∘    β‰‘βŸ¨ F-∘ _ _ βŸ©β‰‘
  F₁ ( , g) E.∘ F₁ (f , ∎

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

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

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

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