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)
where


# Bifunctorsπ

private
module C = Precategory C
module D = Precategory D
module E = Precategory E

open Functor F public


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-β _ _