Bifunctor.idr

Bifunctors

Using the product of categories we can define Bifunctors a functor using a product of categories in the codomain.

  Bifunctor : Type
  Bifunctor = (c1 × c2) ->> c3

Given a functor $B:{\mathcal{C}}_1\times {\mathcal{C}}_2\to {\mathcal{C}}_3$ and $x\in {\mathcal{C}}_1$ we can apply $B$ to $x$ and obtain a functor $B(x):{\mathcal{C}}_2\to {\mathcal{C}}_3$.

public export
applyBifunctor : {0 o1, o2, o3 : Type} ->
                 {a : Category o1} ->
                 {0 b : Category o2} ->
                 {0 c : Category o3} ->
    o1 -> Bifunctor a b c -> b ->> c
applyBifunctor x mult = MkFunctor
  (curry mult.mapObj x)
  (\k, l, m => mult.mapHom (x && k) (x && l) (a.id x && m))
  (\v => mult.presId (x && v) )
  (\ax, bx, cx, f, g =>
      cong (mult .mapHom (x && ?) (x && ?)) (
      cong (&& (|:>) b f g) (sym (a.idLeft _ _ (a.id x)))) `trans`
      mult.presComp (x && ax) (x && bx) (x && cx) (a.id x && f) (a.id x && g))
 
public export
applyBifunctor' : {0 a : Category o} -> {b : Category o} -> o -> Bifunctor a b c -> a ->> c
applyBifunctor' x mult = MkFunctor
  (\y => mult.mapObj (y && x))
  (\k, l, m => mult.mapHom (k && x) (l && x) (m && b.id x))
  (\v => mult.presId (v && x))
  (\ax, bx, cx, f, g =>
      (cong (mult .mapHom (? && x) (? && x))
      $ cong ((|:>) a f g &&)
      $ sym $ b.idRight _ _ $ b.id x) `trans`
      mult.presComp (ax && x) (bx && x) (cx && x) (f && b.id x) (g && b.id x))

We can relate our notion of categorical products with the product of categories by stating that given a category $\mathcal{C}$ with products, we can define a functor $\mathcal{C}\ast \mathcal{C}\to \mathcal{C}$ that maps each objects $|\mathcal{C}\times \mathcal{C}|$ to $|\mathcal{C}|$ using its product, and the product’s universal property to combine morphisms.

public export
ProductFunctor : {c : Category o} -> HasProduct c -> Bifunctor c c c
ProductFunctor (MkProd pair pi1 pi2 prod prodLeft prodRight uniq) = MkFunctor
  (uncurry pair)
  (\_, _, (m1 && m2) => prod ((|:>) c pi1 m1)
                             ((|:>) c pi2 m2))
-- proofs in appendix

public export 0
Bendo : Category o -> Type
Bendo c = c × c ->> c