Bifunctor.idr

As a step toward giving evidence that $\mathcal{C}ont$ is monoidal in $⊳$ we give its definitions as a bifunctor in $\mathcal{C}ont$.

Proposition

The sequencing product forms a bifunctor in $\mathcal{C}ont$.

(~▷~) :
  {0 a, a', b, b' : Container} ->
  (a =%> a') -> (b =%> b') -> a ▷ b =%> a' ▷ b'
(~▷~) m1 m2 = (<!)
  (\x => MkEx (m1.fwd x.ex1)
              (\y => m2.fwd (x.ex2 (m1.bwd x.ex1 y))))
  (\x, y => (m1.bwd x.ex1 y.π1)
         ## m2.bwd (x.ex2 (m1.bwd x.ex1 y.π1)) y.π2)