Monoidal.idr

public export
unitL : I ⊗ a =&> a
unitL = !! \x => x.π2 ## (() &&)
 
public export
unitR : a ⊗ I =&> a
unitR = !! \x => x.π1 ## (&& ())
 
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
 
public export
TensorMonoidal : Monoidal Cont
TensorMonoidal = MkMonoidal
  TensorBifunctor
  I
  alpha
  ?ddd
  ?eee