Monoidal.idr

unitL : I ⊗ a =%> a
unitL = π2 <! (\_ => (() &&))
 
public export
unitR : a ⊗ I =%> a
unitR = π1 <! (\_ => (&&()))

From this we can build the proof that it is a monoidal product in $\mathcal{C}ont$. We use the bifunctor just defined TensorBifunctor, we call it $F$ in diagrams for brevity.

Proposition

The tensor product forms a monoidal structure in $\mathcal{C}ont$

public export
TensorMonoidal : Monoidal Cont
TensorMonoidal = MkMonoidal
    TensorBifunctor
    I
    alpha
    leftUnit
    rightUnit
  where

For the tensor to be monoidal, we need to prove that it is associative. We do this by providing a natural isomorphism between the functors $id\times F;F$ and $F\times id;F$. Due to the nature of programming, we need to add an associator to ensure the functors share the same domain and codomain:

• $f1:Cont\times (Cont\times Cont)\to Cont=id\times F;F$
• $f2:Cont\times (Cont\times Cont)\to Cont=assocR;F\times id;F$

The essence of the natural isomorphism for associativity is captured by the diagram:

The proof itself is routine:

  alpha : let f1, f2 : (Cont × (Cont × Cont)) ->> Cont
              f1 = ((idF Cont) `pair` TensorBifunctor) ⨾⨾ TensorBifunctor
              f2 = assocR {a = Cont, b = Cont, c = Cont}
                   ⨾⨾ ((TensorBifunctor `pair` idF Cont) ⨾⨾ TensorBifunctor)
          in f1 =~= f2
  alpha = MkNaturalIsomorphism
        (MkNT
            (\v => assocR <! (\x, y => assocL y))
            (\a, b, m => Refl))
        (MkNT
            (\v => assocL <! (\x, y => assocR y))
            (\_,_,_ => Refl))
        (\v => cong2Dep
                 (<!)
                 (funExt $ \(a && (b && c)) => Refl)
                 (funExtDep $ \v => funExt $ \(g1 && (g2 && g3)) => Refl))
        (\v => cong2Dep
                 (<!)
                 (funExt $ \((x1 && x2) && x3) => Refl)
                 (funExtDep $ \v => funExt $ \((x1 && x2) && x3) => Refl))

We also need proof that the monoidal unit behaves like a unit on both sides of the bifunctor, again this is done via a natural isomorphism between the identity functor in $\mathcal{C}ont$ and the functor $f:\mathcal{C}ont\to \mathcal{C}ont=unitL;I\times i{d}_{\mathcal{C}ont};F$

The natural isomorphism for left unit is capuring the information in this diagram:

The proof is routine:

  leftUnit : (Bifunctor.unitL ⨾⨾
             (Const I Cont `pair` idF Cont) ⨾⨾
              TensorBifunctor)
              =~= idF Cont
  leftUnit = MkNaturalIsomorphism
        (MkNT
          (\_ => unitL)
          (\_,_,_ => Refl))
        (MkNT
          (\_ =>
            (MkUnit &&) <! (\_ => π2))
          (\_,_,_ => Refl))
        (\c => cong2Dep
          (<!)
          (funExt $ \(() && a) => Refl)
          (funExtDep $ \x => funExt $ \(() && b) => Refl))
        (\_ => Refl)

We do the same for the right unit:

  rightUnit : (Bifunctor.unitR ⨾⨾
              (idF Cont `pair` Const I Cont) ⨾⨾
               TensorBifunctor)
               =~= idF Cont
  rightUnit = MkNaturalIsomorphism
      (MkNT
        (\v => unitR)
        (\a, b, m => Refl))
      (MkNT
        (\v => (&& ()) <! (\_ => π1))
        (\_,_,_ => Refl))
      (\v => cong2Dep
        (<!)
        (funExt $ \(x1 && ()) => Refl)
        (funExtDep $ \v => funExt $ \(w && ()) => Refl))
      (\_ => Refl)

Proposition

A monoid object with regards to the tensor product forms an applicative functor in $Set$.

export %hint
ApplicativeFromMonoid :
  (m : MonoidObject {o = Container, cat = Cont} TensorMonoidal) => Applicative (Ex m.obj)
ApplicativeFromMonoid {m }
  = MkApplicative
    (\x => MkEx (m.η.fwd ()) (const x))
    (\(MkEx lf1 lf2), (MkEx lx1 lx2) =>
         MkEx (m.mult.fwd (lf1 && lx1))
           (\z => let ff = m.mult.bwd (lf1 && lx1) z
                  in lf2 ff.π1 (lx2 ff.π2)))