Bifunctor.idr

The choice of two containers is functorial, that is, given two lenses a =%> a' and b =%> b', we can build the lens a + b =%> a' + b'. We see this with the implementation of (~+~) which will be the map on morphisms of our bifunctor.

Proposition

There is a bimap function on the coproduct of containers.

(~+~) : a =%> a' -> b =%> b' -> (a + b) =%> (a' + b')
(~+~) x y =
  (bimap x.fwd y.fwd) <!
  (dchoice (\xy => x.bwd xy)
           (\xy => y.bwd xy)
           {c = \xa => (a' + b').response (bimap x.fwd y.fwd xa) ->
                       choice (a .response) (b .response) xa}
  )

Using our bimap function we build the coproduct bifunctor on the category Cont

Proposition

Coproducts form a bifunctor in $\mathcal{C}ont$.

CoprodContBifunctor : Bifunctor Cont Cont Cont
CoprodContBifunctor = MkFunctor
  (Product.uncurry (+))
  (\_, _, m => m.π1 ~+~ m.π2)
  -- proofs in appendix

Additionally, we provide a couple of utilities related to coproducts

Proposition

There is a diagonal map $a+a\to a$.

dia : a + a =%> a
dia = dia <! dchoice (\_ => id) (\_ => id)

Additionally, we define injection maps for our coproduct.

Proposition

There are two injection maps $inr:b\to a+b$ and $inl:a\to a+b$.

inr : b =%> a + b
inr = (+>) <! (\x => id)

inl : a =%> a + b
inl = (<+) <! (\x => id)

coprod : a =%> c -> b =%> c -> a + b =%> c
coprod f g = f ~+~ g |%> dia

Proposition

The category of containers has coproducts via $(+)$

contCoprod : HasProduct (Cont .op)