Bifunctor.idr

Tensor is a Bifunctor in $C o n t^{#}$

This definition is necessary to define the fact that $C o n t^{#}$ is monoidal.

We extract the map on morphisms as it is quite handy to use directly.

(~⊗#~) : (a =#> b) -> (a' =#> b') -> a ⊗ a' =#> b ⊗ b'
(~⊗#~) x y = MkCartDepLens (bimap x.cfwd y.cfwd)
    (\v => IsoProd (x.cbwd v.π1) (y.cbwd v.π2))

Using it we define the bifunctor $C o n t^{#} \times C o n t^{#} \to C o n t^{#}$ .

Proposition

Tensor forms a bifunctor $C o n t^{#} \times C o n t^{#} \to C o n t^{#}$

TensorBifunctorCart : Bifunctor ContCart ContCart ContCart
TensorBifunctorCart = MkFunctor
    (uncurry (⊗))
    (\x, y, m => m.π1 ~⊗#~ m.π2)
    -- proofs in appendix