Bifunctor.idr

The continuation product is not a monoidal product on containers, rather, it is an action of $\mathcal{C}on{t}^{\#}$ on $\mathcal{C}ont$. To prove this, we start by proving that it’s a bifunctor $\mathcal{C}on{t}^{\#}\times \mathcal{C}ont\to \mathcal{C}ont$.

• update replace to transport

Once the backward map is defined, we can use the same implementation as ▷ as a bifunctor for the forward map to build our map ~▷~.

public export
(~▶~) :
    {0 a, a', b, b' : Container} ->
    (a =#> a') -> (b =%> b') ->
    a ▶ b =%> a' ▶ b'
(~▶~) m1 m2 =
    (exBimap (toLens a a' m1) m2.fwd) <!
    (bimapCompBwd m1 m2)

This definition is the one that will be used most often when dealing with monads on containers that involve the continuation product ▶, like Maybe. Because of this very special case, I provide a partially applied verion of this map so that we can treat monads from actions as functors.

public export
contFunctor :
    {0 a, x, y: Container} ->
    (x =%> y) ->
    a ▶ x =%> a ▶ y
contFunctor = (identity a ~▶~)

Proposition

Universal composition forms a bifunctor $\mathcal{C}on{t}^{\#}\times \mathcal{C}ont\to \mathcal{C}ont$

public export
ForallSeqBifunctor : Bifunctor ContCart Cont Cont
ForallSeqBifunctor = MkFunctor
  (uncurry (▶))
  (\x, y, m => m.π1 ~▶~ m.π2)
  (\x => depLensEqToEq $ MkDepLensEq
      (\vx => exEqToEq $ MkExEq Refl (\_ => cong vx.ex2 (applyRefl' ? ?)))
      (\vx, vy => bimapIdentity x.π1 x.π2 vx vy))
  (\a, b, c, f, g => preservesComposition _ _ _ _)